Theorem iununi 2037

Description: A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33.

Assertion

Ref	Expression
iununi	⊢ ((B = ∅ → A = ∅) ↔ (A ∪ ∪B) = ∪x ∈ B (A ∪ x))

Distinct variable group(s):   x,A   x,B

Proof of Theorem iununi

Step	Hyp	Ref	Expression
1		imor 204	. . . . . 6 ⊢ ((B = ∅ → A = ∅) ↔ (¬ B = ∅ ∨ A = ∅))
2		r19.45zv 1770	. . . . . . . 8 ⊢ (¬ B = ∅ → (∃x ∈ B (y ∈ A ∨ y ∈ x) ↔ (y ∈ A ∨ ∃x ∈ B y ∈ x)))
3		n0i 1712	. . . . . . . . . 10 ⊢ (y ∈ A → ¬ A = ∅)
4	3	con2i 89	. . . . . . . . 9 ⊢ (A = ∅ → ¬ y ∈ A)
5		biorf 551	. . . . . . . . . . 11 ⊢ (¬ y ∈ A → (y ∈ x ↔ (y ∈ A ∨ y ∈ x)))
6	5	birexdv 1220	. . . . . . . . . 10 ⊢ (¬ y ∈ A → (∃x ∈ B y ∈ x ↔ ∃x ∈ B (y ∈ A ∨ y ∈ x)))
7		biorf 551	. . . . . . . . . 10 ⊢ (¬ y ∈ A → (∃x ∈ B y ∈ x ↔ (y ∈ A ∨ ∃x ∈ B y ∈ x)))
8	6, 7	bitr3d 408	. . . . . . . . 9 ⊢ (¬ y ∈ A → (∃x ∈ B (y ∈ A ∨ y ∈ x) ↔ (y ∈ A ∨ ∃x ∈ B y ∈ x)))
9	4, 8	syl 12	. . . . . . . 8 ⊢ (A = ∅ → (∃x ∈ B (y ∈ A ∨ y ∈ x) ↔ (y ∈ A ∨ ∃x ∈ B y ∈ x)))
10	2, 9	jaoi 275	. . . . . . 7 ⊢ ((¬ B = ∅ ∨ A = ∅) → (∃x ∈ B (y ∈ A ∨ y ∈ x) ↔ (y ∈ A ∨ ∃x ∈ B y ∈ x)))
11	10	bicomd 399	. . . . . 6 ⊢ ((¬ B = ∅ ∨ A = ∅) → ((y ∈ A ∨ ∃x ∈ B y ∈ x) ↔ ∃x ∈ B (y ∈ A ∨ y ∈ x)))
12	1, 11	sylbi 174	. . . . 5 ⊢ ((B = ∅ → A = ∅) → ((y ∈ A ∨ ∃x ∈ B y ∈ x) ↔ ∃x ∈ B (y ∈ A ∨ y ∈ x)))
13		elun 1601	. . . . . 6 ⊢ (y ∈ (A ∪ x) ↔ (y ∈ A ∨ y ∈ x))
14	13	birex 1224	. . . . 5 ⊢ (∃x ∈ B y ∈ (A ∪ x) ↔ ∃x ∈ B (y ∈ A ∨ y ∈ x))
15	12, 14	syl6bbr 416	. . . 4 ⊢ ((B = ∅ → A = ∅) → ((y ∈ A ∨ ∃x ∈ B y ∈ x) ↔ ∃x ∈ B y ∈ (A ∪ x)))
16		elun 1601	. . . . 5 ⊢ (y ∈ (A ∪ ∪B) ↔ (y ∈ A ∨ y ∈ ∪B))
17		eluni2 1923	. . . . . 6 ⊢ (y ∈ ∪B ↔ ∃x ∈ B y ∈ x)
18	17	orbi2i 214	. . . . 5 ⊢ ((y ∈ A ∨ y ∈ ∪B) ↔ (y ∈ A ∨ ∃x ∈ B y ∈ x))
19	16, 18	bitr 151	. . . 4 ⊢ (y ∈ (A ∪ ∪B) ↔ (y ∈ A ∨ ∃x ∈ B y ∈ x))
20		eliun 1998	. . . 4 ⊢ (y ∈ ∪x ∈ B (A ∪ x) ↔ ∃x ∈ B y ∈ (A ∪ x))
21	15, 19, 20	3bitr4g 428	. . 3 ⊢ ((B = ∅ → A = ∅) → (y ∈ (A ∪ ∪B) ↔ y ∈ ∪x ∈ B (A ∪ x)))
22	21	cleqrd 1100	. 2 ⊢ ((B = ∅ → A = ∅) → (A ∪ ∪B) = ∪x ∈ B (A ∪ x))
23		eleq2 1150	. . . . . . . . 9 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → (y ∈ (A ∪ ∪B) ↔ y ∈ ∪x ∈ B (A ∪ x)))
24		eluni 1922	. . . . . . . . . . 11 ⊢ (y ∈ ∪B ↔ ∃x(y ∈ x ∧ x ∈ B))
25	24	orbi2i 214	. . . . . . . . . 10 ⊢ ((y ∈ A ∨ y ∈ ∪B) ↔ (y ∈ A ∨ ∃x(y ∈ x ∧ x ∈ B)))
26		ax-17 925	. . . . . . . . . . 11 ⊢ (y ∈ A → ∀x y ∈ A)
27	26	19.45 769	. . . . . . . . . 10 ⊢ (∃x(y ∈ A ∨ (y ∈ x ∧ x ∈ B)) ↔ (y ∈ A ∨ ∃x(y ∈ x ∧ x ∈ B)))
28	25, 16, 27	3bitr4 158	. . . . . . . . 9 ⊢ (y ∈ (A ∪ ∪B) ↔ ∃x(y ∈ A ∨ (y ∈ x ∧ x ∈ B)))
29		df-rex 1206	. . . . . . . . . 10 ⊢ (∃x ∈ B y ∈ (A ∪ x) ↔ ∃x(x ∈ B ∧ y ∈ (A ∪ x)))
30	20, 29	bitr 151	. . . . . . . . 9 ⊢ (y ∈ ∪x ∈ B (A ∪ x) ↔ ∃x(x ∈ B ∧ y ∈ (A ∪ x)))
31	23, 28, 30	3bitr3g 427	. . . . . . . 8 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → (∃x(y ∈ A ∨ (y ∈ x ∧ x ∈ B)) ↔ ∃x(x ∈ B ∧ y ∈ (A ∪ x))))
32	31	biimpd 135	. . . . . . 7 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → (∃x(y ∈ A ∨ (y ∈ x ∧ x ∈ B)) → ∃x(x ∈ B ∧ y ∈ (A ∪ x))))
33		19.39 761	. . . . . . 7 ⊢ ((∃x(y ∈ A ∨ (y ∈ x ∧ x ∈ B)) → ∃x(x ∈ B ∧ y ∈ (A ∪ x))) → ∃x((y ∈ A ∨ (y ∈ x ∧ x ∈ B)) → (x ∈ B ∧ y ∈ (A ∪ x))))
34		orc 225	. . . . . . . . 9 ⊢ (y ∈ A → (y ∈ A ∨ (y ∈ x ∧ x ∈ B)))
35		pm3.26 256	. . . . . . . . 9 ⊢ ((x ∈ B ∧ y ∈ (A ∪ x)) → x ∈ B)
36	34, 35	syl34 20	. . . . . . . 8 ⊢ (((y ∈ A ∨ (y ∈ x ∧ x ∈ B)) → (x ∈ B ∧ y ∈ (A ∪ x))) → (y ∈ A → x ∈ B))
37	36	19.22i 723	. . . . . . 7 ⊢ (∃x((y ∈ A ∨ (y ∈ x ∧ x ∈ B)) → (x ∈ B ∧ y ∈ (A ∪ x))) → ∃x(y ∈ A → x ∈ B))
38	32, 33, 37	3syl 21	. . . . . 6 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → ∃x(y ∈ A → x ∈ B))
39		19.37v 961	. . . . . 6 ⊢ (∃x(y ∈ A → x ∈ B) ↔ (y ∈ A → ∃x x ∈ B))
40	38, 39	sylib 173	. . . . 5 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → (y ∈ A → ∃x x ∈ B))
41	40	19.23adv 954	. . . 4 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → (∃y y ∈ A → ∃x x ∈ B))
42		n0 1714	. . . 4 ⊢ (¬ A = ∅ ↔ ∃y y ∈ A)
43		n0 1714	. . . 4 ⊢ (¬ B = ∅ ↔ ∃x x ∈ B)
44	41, 42, 43	3imtr4g 426	. . 3 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → (¬ A = ∅ → ¬ B = ∅))
45	44	a3d 70	. 2 ⊢ ((A ∪ ∪B) = ∪x ∈ B (A ∪ x) → (B = ∅ → A = ∅))
46	22, 45	impbi 139	1 ⊢ ((B = ∅ → A = ∅) ↔ (A ∪ ∪B) = ∪x ∈ B (A ∪ x))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∃wex 678   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∃wrex 1202   ∪ cun 1485  ∅c0 1707  ∪cuni 1919  ∪ciun 1994

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-nul 1708  df-uni 1920  df-iun 1996

metamath.org