This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∪ ∪ 𝐴 = ∪ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴 ) }