Metamath Proof Explorer

Theorem ituniiun

Description: Unwrap an iterated union from the "other end". (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Hypothesis ituni.u 
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
Assertion ituniiun 
|- ( A e. V -> ( ( U ` A ) ` suc B ) = U_ a e. A ( ( U ` a ) ` B ) )

Proof

Step Hyp Ref Expression
1 ituni.u 
 |-  U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
2 fveq2 
 |-  ( b = A -> ( U ` b ) = ( U ` A ) )
3 2 fveq1d 
 |-  ( b = A -> ( ( U ` b ) ` suc B ) = ( ( U ` A ) ` suc B ) )
4 iuneq1 
 |-  ( b = A -> U_ a e. b ( ( U ` a ) ` B ) = U_ a e. A ( ( U ` a ) ` B ) )
5 3 4 eqeq12d 
 |-  ( b = A -> ( ( ( U ` b ) ` suc B ) = U_ a e. b ( ( U ` a ) ` B ) <-> ( ( U ` A ) ` suc B ) = U_ a e. A ( ( U ` a ) ` B ) ) )
6 suceq 
 |-  ( d = (/) -> suc d = suc (/) )
7 6 fveq2d 
 |-  ( d = (/) -> ( ( U ` b ) ` suc d ) = ( ( U ` b ) ` suc (/) ) )
8 fveq2 
 |-  ( d = (/) -> ( ( U ` a ) ` d ) = ( ( U ` a ) ` (/) ) )
9 8 iuneq2d 
 |-  ( d = (/) -> U_ a e. b ( ( U ` a ) ` d ) = U_ a e. b ( ( U ` a ) ` (/) ) )
10 7 9 eqeq12d 
 |-  ( d = (/) -> ( ( ( U ` b ) ` suc d ) = U_ a e. b ( ( U ` a ) ` d ) <-> ( ( U ` b ) ` suc (/) ) = U_ a e. b ( ( U ` a ) ` (/) ) ) )
11 suceq 
 |-  ( d = c -> suc d = suc c )
12 11 fveq2d 
 |-  ( d = c -> ( ( U ` b ) ` suc d ) = ( ( U ` b ) ` suc c ) )
13 fveq2 
 |-  ( d = c -> ( ( U ` a ) ` d ) = ( ( U ` a ) ` c ) )
14 13 iuneq2d 
 |-  ( d = c -> U_ a e. b ( ( U ` a ) ` d ) = U_ a e. b ( ( U ` a ) ` c ) )
15 12 14 eqeq12d 
 |-  ( d = c -> ( ( ( U ` b ) ` suc d ) = U_ a e. b ( ( U ` a ) ` d ) <-> ( ( U ` b ) ` suc c ) = U_ a e. b ( ( U ` a ) ` c ) ) )
16 suceq 
 |-  ( d = suc c -> suc d = suc suc c )
17 16 fveq2d 
 |-  ( d = suc c -> ( ( U ` b ) ` suc d ) = ( ( U ` b ) ` suc suc c ) )
18 fveq2 
 |-  ( d = suc c -> ( ( U ` a ) ` d ) = ( ( U ` a ) ` suc c ) )
19 18 iuneq2d 
 |-  ( d = suc c -> U_ a e. b ( ( U ` a ) ` d ) = U_ a e. b ( ( U ` a ) ` suc c ) )
20 17 19 eqeq12d 
 |-  ( d = suc c -> ( ( ( U ` b ) ` suc d ) = U_ a e. b ( ( U ` a ) ` d ) <-> ( ( U ` b ) ` suc suc c ) = U_ a e. b ( ( U ` a ) ` suc c ) ) )
21 suceq 
 |-  ( d = B -> suc d = suc B )
22 21 fveq2d 
 |-  ( d = B -> ( ( U ` b ) ` suc d ) = ( ( U ` b ) ` suc B ) )
23 fveq2 
 |-  ( d = B -> ( ( U ` a ) ` d ) = ( ( U ` a ) ` B ) )
24 23 iuneq2d 
 |-  ( d = B -> U_ a e. b ( ( U ` a ) ` d ) = U_ a e. b ( ( U ` a ) ` B ) )
25 22 24 eqeq12d 
 |-  ( d = B -> ( ( ( U ` b ) ` suc d ) = U_ a e. b ( ( U ` a ) ` d ) <-> ( ( U ` b ) ` suc B ) = U_ a e. b ( ( U ` a ) ` B ) ) )
26 uniiun 
 |-  U. b = U_ a e. b a
27 1 itunisuc 
 |-  ( ( U ` b ) ` suc (/) ) = U. ( ( U ` b ) ` (/) )
28 1 ituni0 
 |-  ( b e. _V -> ( ( U ` b ) ` (/) ) = b )
29 28 elv 
 |-  ( ( U ` b ) ` (/) ) = b
30 29 unieqi 
 |-  U. ( ( U ` b ) ` (/) ) = U. b
31 27 30 eqtri 
 |-  ( ( U ` b ) ` suc (/) ) = U. b
32 1 ituni0 
 |-  ( a e. b -> ( ( U ` a ) ` (/) ) = a )
33 32 iuneq2i 
 |-  U_ a e. b ( ( U ` a ) ` (/) ) = U_ a e. b a
34 26 31 33 3eqtr4i 
 |-  ( ( U ` b ) ` suc (/) ) = U_ a e. b ( ( U ` a ) ` (/) )
35 1 itunisuc 
 |-  ( ( U ` b ) ` suc suc c ) = U. ( ( U ` b ) ` suc c )
36 unieq 
 |-  ( ( ( U ` b ) ` suc c ) = U_ a e. b ( ( U ` a ) ` c ) -> U. ( ( U ` b ) ` suc c ) = U. U_ a e. b ( ( U ` a ) ` c ) )
37 1 itunisuc 
 |-  ( ( U ` a ) ` suc c ) = U. ( ( U ` a ) ` c )
38 37 a1i 
 |-  ( a e. b -> ( ( U ` a ) ` suc c ) = U. ( ( U ` a ) ` c ) )
39 38 iuneq2i 
 |-  U_ a e. b ( ( U ` a ) ` suc c ) = U_ a e. b U. ( ( U ` a ) ` c )
40 iuncom4 
 |-  U_ a e. b U. ( ( U ` a ) ` c ) = U. U_ a e. b ( ( U ` a ) ` c )
41 39 40 eqtr2i 
 |-  U. U_ a e. b ( ( U ` a ) ` c ) = U_ a e. b ( ( U ` a ) ` suc c )
42 36 41 eqtrdi 
 |-  ( ( ( U ` b ) ` suc c ) = U_ a e. b ( ( U ` a ) ` c ) -> U. ( ( U ` b ) ` suc c ) = U_ a e. b ( ( U ` a ) ` suc c ) )
43 35 42 eqtrid 
 |-  ( ( ( U ` b ) ` suc c ) = U_ a e. b ( ( U ` a ) ` c ) -> ( ( U ` b ) ` suc suc c ) = U_ a e. b ( ( U ` a ) ` suc c ) )
44 43 a1i 
 |-  ( c e. _om -> ( ( ( U ` b ) ` suc c ) = U_ a e. b ( ( U ` a ) ` c ) -> ( ( U ` b ) ` suc suc c ) = U_ a e. b ( ( U ` a ) ` suc c ) ) )
45 10 15 20 25 34 44 finds 
 |-  ( B e. _om -> ( ( U ` b ) ` suc B ) = U_ a e. b ( ( U ` a ) ` B ) )
46 iun0 
 |-  U_ a e. b (/) = (/)
47 46 eqcomi 
 |-  (/) = U_ a e. b (/)
48 peano2b 
 |-  ( B e. _om <-> suc B e. _om )
49 vex 
 |-  b e. _V
50 1 itunifn 
 |-  ( b e. _V -> ( U ` b ) Fn _om )
51 fndm 
 |-  ( ( U ` b ) Fn _om -> dom ( U ` b ) = _om )
52 49 50 51 mp2b 
 |-  dom ( U ` b ) = _om
53 52 eleq2i 
 |-  ( suc B e. dom ( U ` b ) <-> suc B e. _om )
54 48 53 bitr4i 
 |-  ( B e. _om <-> suc B e. dom ( U ` b ) )
55 ndmfv 
 |-  ( -. suc B e. dom ( U ` b ) -> ( ( U ` b ) ` suc B ) = (/) )
56 54 55 sylnbi 
 |-  ( -. B e. _om -> ( ( U ` b ) ` suc B ) = (/) )
57 vex 
 |-  a e. _V
58 1 itunifn 
 |-  ( a e. _V -> ( U ` a ) Fn _om )
59 fndm 
 |-  ( ( U ` a ) Fn _om -> dom ( U ` a ) = _om )
60 57 58 59 mp2b 
 |-  dom ( U ` a ) = _om
61 60 eleq2i 
 |-  ( B e. dom ( U ` a ) <-> B e. _om )
62 ndmfv 
 |-  ( -. B e. dom ( U ` a ) -> ( ( U ` a ) ` B ) = (/) )
63 61 62 sylnbir 
 |-  ( -. B e. _om -> ( ( U ` a ) ` B ) = (/) )
64 63 iuneq2d 
 |-  ( -. B e. _om -> U_ a e. b ( ( U ` a ) ` B ) = U_ a e. b (/) )
65 47 56 64 3eqtr4a 
 |-  ( -. B e. _om -> ( ( U ` b ) ` suc B ) = U_ a e. b ( ( U ` a ) ` B ) )
66 45 65 pm2.61i 
 |-  ( ( U ` b ) ` suc B ) = U_ a e. b ( ( U ` a ) ` B )
67 5 66 vtoclg 
 |-  ( A e. V -> ( ( U ` A ) ` suc B ) = U_ a e. A ( ( U ` a ) ` B ) )