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 
|- U. U. A = U. { x | E. y ( x = U. y /\ y e. A ) }

Proof

Step Hyp Ref Expression
1 eluni 
 |-  ( u e. U. A <-> E. y ( u e. y /\ y e. A ) )
2 1 anbi2i 
 |-  ( ( z e. u /\ u e. U. A ) <-> ( z e. u /\ E. y ( u e. y /\ y e. A ) ) )
3 2 exbii 
 |-  ( E. u ( z e. u /\ u e. U. A ) <-> E. u ( z e. u /\ E. y ( u e. y /\ y e. A ) ) )
4 19.42v 
 |-  ( E. y ( z e. u /\ ( u e. y /\ y e. A ) ) <-> ( z e. u /\ E. y ( u e. y /\ y e. A ) ) )
5 4 bicomi 
 |-  ( ( z e. u /\ E. y ( u e. y /\ y e. A ) ) <-> E. y ( z e. u /\ ( u e. y /\ y e. A ) ) )
6 5 exbii 
 |-  ( E. u ( z e. u /\ E. y ( u e. y /\ y e. A ) ) <-> E. u E. y ( z e. u /\ ( u e. y /\ y e. A ) ) )
7 excom 
 |-  ( E. u E. y ( z e. u /\ ( u e. y /\ y e. A ) ) <-> E. y E. u ( z e. u /\ ( u e. y /\ y e. A ) ) )
8 anass 
 |-  ( ( ( z e. u /\ u e. y ) /\ y e. A ) <-> ( z e. u /\ ( u e. y /\ y e. A ) ) )
9 ancom 
 |-  ( ( ( z e. u /\ u e. y ) /\ y e. A ) <-> ( y e. A /\ ( z e. u /\ u e. y ) ) )
10 8 9 bitr3i 
 |-  ( ( z e. u /\ ( u e. y /\ y e. A ) ) <-> ( y e. A /\ ( z e. u /\ u e. y ) ) )
11 10 2exbii 
 |-  ( E. y E. u ( z e. u /\ ( u e. y /\ y e. A ) ) <-> E. y E. u ( y e. A /\ ( z e. u /\ u e. y ) ) )
12 exdistr 
 |-  ( E. y E. u ( y e. A /\ ( z e. u /\ u e. y ) ) <-> E. y ( y e. A /\ E. u ( z e. u /\ u e. y ) ) )
13 7 11 12 3bitri 
 |-  ( E. u E. y ( z e. u /\ ( u e. y /\ y e. A ) ) <-> E. y ( y e. A /\ E. u ( z e. u /\ u e. y ) ) )
14 eluni 
 |-  ( z e. U. y <-> E. u ( z e. u /\ u e. y ) )
15 14 bicomi 
 |-  ( E. u ( z e. u /\ u e. y ) <-> z e. U. y )
16 15 anbi2i 
 |-  ( ( y e. A /\ E. u ( z e. u /\ u e. y ) ) <-> ( y e. A /\ z e. U. y ) )
17 16 exbii 
 |-  ( E. y ( y e. A /\ E. u ( z e. u /\ u e. y ) ) <-> E. y ( y e. A /\ z e. U. y ) )
18 6 13 17 3bitri 
 |-  ( E. u ( z e. u /\ E. y ( u e. y /\ y e. A ) ) <-> E. y ( y e. A /\ z e. U. y ) )
19 vuniex 
 |-  U. y e. _V
20 eleq2 
 |-  ( v = U. y -> ( z e. v <-> z e. U. y ) )
21 19 20 ceqsexv 
 |-  ( E. v ( v = U. y /\ z e. v ) <-> z e. U. y )
22 exancom 
 |-  ( E. v ( v = U. y /\ z e. v ) <-> E. v ( z e. v /\ v = U. y ) )
23 21 22 bitr3i 
 |-  ( z e. U. y <-> E. v ( z e. v /\ v = U. y ) )
24 23 anbi2i 
 |-  ( ( y e. A /\ z e. U. y ) <-> ( y e. A /\ E. v ( z e. v /\ v = U. y ) ) )
25 19.42v 
 |-  ( E. v ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> ( y e. A /\ E. v ( z e. v /\ v = U. y ) ) )
26 ancom 
 |-  ( ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> ( ( z e. v /\ v = U. y ) /\ y e. A ) )
27 anass 
 |-  ( ( ( z e. v /\ v = U. y ) /\ y e. A ) <-> ( z e. v /\ ( v = U. y /\ y e. A ) ) )
28 26 27 bitri 
 |-  ( ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> ( z e. v /\ ( v = U. y /\ y e. A ) ) )
29 28 exbii 
 |-  ( E. v ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) )
30 24 25 29 3bitr2i 
 |-  ( ( y e. A /\ z e. U. y ) <-> E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) )
31 30 exbii 
 |-  ( E. y ( y e. A /\ z e. U. y ) <-> E. y E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) )
32 excom 
 |-  ( E. y E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) <-> E. v E. y ( z e. v /\ ( v = U. y /\ y e. A ) ) )
33 exdistr 
 |-  ( E. v E. y ( z e. v /\ ( v = U. y /\ y e. A ) ) <-> E. v ( z e. v /\ E. y ( v = U. y /\ y e. A ) ) )
34 vex 
 |-  v e. _V
35 eqeq1 
 |-  ( x = v -> ( x = U. y <-> v = U. y ) )
36 35 anbi1d 
 |-  ( x = v -> ( ( x = U. y /\ y e. A ) <-> ( v = U. y /\ y e. A ) ) )
37 36 exbidv 
 |-  ( x = v -> ( E. y ( x = U. y /\ y e. A ) <-> E. y ( v = U. y /\ y e. A ) ) )
38 34 37 elab 
 |-  ( v e. { x | E. y ( x = U. y /\ y e. A ) } <-> E. y ( v = U. y /\ y e. A ) )
39 38 bicomi 
 |-  ( E. y ( v = U. y /\ y e. A ) <-> v e. { x | E. y ( x = U. y /\ y e. A ) } )
40 39 anbi2i 
 |-  ( ( z e. v /\ E. y ( v = U. y /\ y e. A ) ) <-> ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) )
41 40 exbii 
 |-  ( E. v ( z e. v /\ E. y ( v = U. y /\ y e. A ) ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) )
42 33 41 bitri 
 |-  ( E. v E. y ( z e. v /\ ( v = U. y /\ y e. A ) ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) )
43 31 32 42 3bitri 
 |-  ( E. y ( y e. A /\ z e. U. y ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) )
44 3 18 43 3bitri 
 |-  ( E. u ( z e. u /\ u e. U. A ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) )
45 44 abbii 
 |-  { z | E. u ( z e. u /\ u e. U. A ) } = { z | E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) }
46 df-uni 
 |-  U. U. A = { z | E. u ( z e. u /\ u e. U. A ) }
47 df-uni 
 |-  U. { x | E. y ( x = U. y /\ y e. A ) } = { z | E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) }
48 45 46 47 3eqtr4i 
 |-  U. U. A = U. { x | E. y ( x = U. y /\ y e. A ) }