Theorem iununi 2037

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

Assertion

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

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196  E.wex 678   e. wel 803   = wceq 1091   e. wcel 1092  E.wrex 1202   u. cun 1485  (/)c0 1707  U.cuni 1919  U.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