Metamath Proof Explorer

Theorem itunisuc

Description: Successor iterated union. (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 itunisuc 
|- ( ( U ` A ) ` suc B ) = U. ( ( U ` A ) ` B )

Proof

Step Hyp Ref Expression
1 ituni.u 
 |-  U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
2 frsuc 
 |-  ( B e. _om -> ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` suc B ) = ( ( y e. _V |-> U. y ) ` ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) ) )
3 fvex 
 |-  ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) e. _V
4 unieq 
 |-  ( a = ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) -> U. a = U. ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) )
5 unieq 
 |-  ( y = a -> U. y = U. a )
6 5 cbvmptv 
 |-  ( y e. _V |-> U. y ) = ( a e. _V |-> U. a )
7 3 uniex 
 |-  U. ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) e. _V
8 4 6 7 fvmpt 
 |-  ( ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) e. _V -> ( ( y e. _V |-> U. y ) ` ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) ) = U. ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) )
9 3 8 ax-mp 
 |-  ( ( y e. _V |-> U. y ) ` ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) ) = U. ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B )
10 2 9 eqtrdi 
 |-  ( B e. _om -> ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` suc B ) = U. ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) )
11 10 adantl 
 |-  ( ( A e. _V /\ B e. _om ) -> ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` suc B ) = U. ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) )
12 1 itunifval 
 |-  ( A e. _V -> ( U ` A ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) )
13 12 fveq1d 
 |-  ( A e. _V -> ( ( U ` A ) ` suc B ) = ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` suc B ) )
14 13 adantr 
 |-  ( ( A e. _V /\ B e. _om ) -> ( ( U ` A ) ` suc B ) = ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` suc B ) )
15 12 fveq1d 
 |-  ( A e. _V -> ( ( U ` A ) ` B ) = ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) )
16 15 adantr 
 |-  ( ( A e. _V /\ B e. _om ) -> ( ( U ` A ) ` B ) = ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) )
17 16 unieqd 
 |-  ( ( A e. _V /\ B e. _om ) -> U. ( ( U ` A ) ` B ) = U. ( ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) ` B ) )
18 11 14 17 3eqtr4d 
 |-  ( ( A e. _V /\ B e. _om ) -> ( ( U ` A ) ` suc B ) = U. ( ( U ` A ) ` B ) )
19 uni0 
 |-  U. (/) = (/)
20 19 eqcomi 
 |-  (/) = U. (/)
21 1 itunifn 
 |-  ( A e. _V -> ( U ` A ) Fn _om )
22 21 fndmd 
 |-  ( A e. _V -> dom ( U ` A ) = _om )
23 22 eleq2d 
 |-  ( A e. _V -> ( suc B e. dom ( U ` A ) <-> suc B e. _om ) )
24 peano2b 
 |-  ( B e. _om <-> suc B e. _om )
25 23 24 bitr4di 
 |-  ( A e. _V -> ( suc B e. dom ( U ` A ) <-> B e. _om ) )
26 25 notbid 
 |-  ( A e. _V -> ( -. suc B e. dom ( U ` A ) <-> -. B e. _om ) )
27 26 biimpar 
 |-  ( ( A e. _V /\ -. B e. _om ) -> -. suc B e. dom ( U ` A ) )
28 ndmfv 
 |-  ( -. suc B e. dom ( U ` A ) -> ( ( U ` A ) ` suc B ) = (/) )
29 27 28 syl 
 |-  ( ( A e. _V /\ -. B e. _om ) -> ( ( U ` A ) ` suc B ) = (/) )
30 22 eleq2d 
 |-  ( A e. _V -> ( B e. dom ( U ` A ) <-> B e. _om ) )
31 30 notbid 
 |-  ( A e. _V -> ( -. B e. dom ( U ` A ) <-> -. B e. _om ) )
32 31 biimpar 
 |-  ( ( A e. _V /\ -. B e. _om ) -> -. B e. dom ( U ` A ) )
33 ndmfv 
 |-  ( -. B e. dom ( U ` A ) -> ( ( U ` A ) ` B ) = (/) )
34 32 33 syl 
 |-  ( ( A e. _V /\ -. B e. _om ) -> ( ( U ` A ) ` B ) = (/) )
35 34 unieqd 
 |-  ( ( A e. _V /\ -. B e. _om ) -> U. ( ( U ` A ) ` B ) = U. (/) )
36 20 29 35 3eqtr4a 
 |-  ( ( A e. _V /\ -. B e. _om ) -> ( ( U ` A ) ` suc B ) = U. ( ( U ` A ) ` B ) )
37 18 36 pm2.61dan 
 |-  ( A e. _V -> ( ( U ` A ) ` suc B ) = U. ( ( U ` A ) ` B ) )
38 0fv 
 |-  ( (/) ` B ) = (/)
39 38 unieqi 
 |-  U. ( (/) ` B ) = U. (/)
40 0fv 
 |-  ( (/) ` suc B ) = (/)
41 19 39 40 3eqtr4ri 
 |-  ( (/) ` suc B ) = U. ( (/) ` B )
42 fvprc 
 |-  ( -. A e. _V -> ( U ` A ) = (/) )
43 42 fveq1d 
 |-  ( -. A e. _V -> ( ( U ` A ) ` suc B ) = ( (/) ` suc B ) )
44 42 fveq1d 
 |-  ( -. A e. _V -> ( ( U ` A ) ` B ) = ( (/) ` B ) )
45 44 unieqd 
 |-  ( -. A e. _V -> U. ( ( U ` A ) ` B ) = U. ( (/) ` B ) )
46 41 43 45 3eqtr4a 
 |-  ( -. A e. _V -> ( ( U ` A ) ` suc B ) = U. ( ( U ` A ) ` B ) )
47 37 46 pm2.61i 
 |-  ( ( U ` A ) ` suc B ) = U. ( ( U ` A ) ` B )