Theorem uniuni

Description: Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007)

	Ref	Expression
Assertion	uniuni	⊢ ∪ ∪ 𝐴 = ∪ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) }

Proof

Step	Hyp	Ref	Expression
1		eluni	⊢ ( 𝑢 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
2	1	anbi2i	⊢ ( ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝐴 ) ↔ ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑦 ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
3	2	exbii	⊢ ( ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝐴 ) ↔ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑦 ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
4		19.42v	⊢ ( ∃ 𝑦 ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑦 ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
5	4	bicomi	⊢ ( ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑦 ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
6	5	exbii	⊢ ( ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑦 ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑢 ∃ 𝑦 ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
7		excom	⊢ ( ∃ 𝑢 ∃ 𝑦 ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑦 ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
8		anass	⊢ ( ( ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
9		ancom	⊢ ( ( ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) )
10	8 9	bitr3i	⊢ ( ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) )
11	10	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑦 ∃ 𝑢 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) )
12		exdistr	⊢ ( ∃ 𝑦 ∃ 𝑢 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) )
13	7 11 12	3bitri	⊢ ( ∃ 𝑢 ∃ 𝑦 ( 𝑧 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) )
14		eluni	⊢ ( 𝑧 ∈ ∪ 𝑦 ↔ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) )
15	14	bicomi	⊢ ( ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ↔ 𝑧 ∈ ∪ 𝑦 )
16	15	anbi2i	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ∪ 𝑦 ) )
17	16	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ∪ 𝑦 ) )
18	6 13 17	3bitri	⊢ ( ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑦 ( 𝑢 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ∪ 𝑦 ) )
19		vuniex	⊢ ∪ 𝑦 ∈ V
20		eleq2	⊢ ( 𝑣 = ∪ 𝑦 → ( 𝑧 ∈ 𝑣 ↔ 𝑧 ∈ ∪ 𝑦 ) )
21	19 20	ceqsexv	⊢ ( ∃ 𝑣 ( 𝑣 = ∪ 𝑦 ∧ 𝑧 ∈ 𝑣 ) ↔ 𝑧 ∈ ∪ 𝑦 )
22		exancom	⊢ ( ∃ 𝑣 ( 𝑣 = ∪ 𝑦 ∧ 𝑧 ∈ 𝑣 ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) )
23	21 22	bitr3i	⊢ ( 𝑧 ∈ ∪ 𝑦 ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) )
24	23	anbi2i	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ∪ 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ) )
25		19.42v	⊢ ( ∃ 𝑣 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ) )
26		ancom	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ) ↔ ( ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ∧ 𝑦 ∈ 𝐴 ) )
27		anass	⊢ ( ( ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
28	26 27	bitri	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
29	28	exbii	⊢ ( ∃ 𝑣 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑣 = ∪ 𝑦 ) ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
30	24 25 29	3bitr2i	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ∪ 𝑦 ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
31	30	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ∪ 𝑦 ) ↔ ∃ 𝑦 ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
32		excom	⊢ ( ∃ 𝑦 ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑣 ∃ 𝑦 ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
33		exdistr	⊢ ( ∃ 𝑣 ∃ 𝑦 ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ ∃ 𝑦 ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
34		vex	⊢ 𝑣 ∈ V
35		eqeq1	⊢ ( 𝑥 = 𝑣 → ( 𝑥 = ∪ 𝑦 ↔ 𝑣 = ∪ 𝑦 ) )
36	35	anbi1d	⊢ ( 𝑥 = 𝑣 → ( ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
37	36	exbidv	⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ↔ ∃ 𝑦 ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) )
38	34 37	elab	⊢ ( 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ↔ ∃ 𝑦 ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
39	38	bicomi	⊢ ( ∃ 𝑦 ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ↔ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } )
40	39	anbi2i	⊢ ( ( 𝑧 ∈ 𝑣 ∧ ∃ 𝑦 ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ) )
41	40	exbii	⊢ ( ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ ∃ 𝑦 ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ) )
42	33 41	bitri	⊢ ( ∃ 𝑣 ∃ 𝑦 ( 𝑧 ∈ 𝑣 ∧ ( 𝑣 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ) )
43	31 32 42	3bitri	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ ∪ 𝑦 ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ) )
44	3 18 43	3bitri	⊢ ( ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝐴 ) ↔ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ) )
45	44	abbii	⊢ { 𝑧 ∣ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝐴 ) } = { 𝑧 ∣ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ) }
46		df-uni	⊢ ∪ ∪ 𝐴 = { 𝑧 ∣ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝐴 ) }
47		df-uni	⊢ ∪ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } = { 𝑧 ∣ ∃ 𝑣 ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } ) }
48	45 46 47	3eqtr4i	⊢ ∪ ∪ 𝐴 = ∪ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) }