Metamath Proof Explorer

Theorem itunitc1

Description: Each union iterate is a member of the transitive closure. (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 itunitc1 
|- ( ( U ` A ) ` B ) C_ ( TC ` A )

Proof

Step Hyp Ref Expression
1 ituni.u 
 |-  U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
2 fveq2 
 |-  ( a = A -> ( U ` a ) = ( U ` A ) )
3 2 fveq1d 
 |-  ( a = A -> ( ( U ` a ) ` B ) = ( ( U ` A ) ` B ) )
4 fveq2 
 |-  ( a = A -> ( TC ` a ) = ( TC ` A ) )
5 3 4 sseq12d 
 |-  ( a = A -> ( ( ( U ` a ) ` B ) C_ ( TC ` a ) <-> ( ( U ` A ) ` B ) C_ ( TC ` A ) ) )
6 fveq2 
 |-  ( b = (/) -> ( ( U ` a ) ` b ) = ( ( U ` a ) ` (/) ) )
7 6 sseq1d 
 |-  ( b = (/) -> ( ( ( U ` a ) ` b ) C_ ( TC ` a ) <-> ( ( U ` a ) ` (/) ) C_ ( TC ` a ) ) )
8 fveq2 
 |-  ( b = c -> ( ( U ` a ) ` b ) = ( ( U ` a ) ` c ) )
9 8 sseq1d 
 |-  ( b = c -> ( ( ( U ` a ) ` b ) C_ ( TC ` a ) <-> ( ( U ` a ) ` c ) C_ ( TC ` a ) ) )
10 fveq2 
 |-  ( b = suc c -> ( ( U ` a ) ` b ) = ( ( U ` a ) ` suc c ) )
11 10 sseq1d 
 |-  ( b = suc c -> ( ( ( U ` a ) ` b ) C_ ( TC ` a ) <-> ( ( U ` a ) ` suc c ) C_ ( TC ` a ) ) )
12 fveq2 
 |-  ( b = B -> ( ( U ` a ) ` b ) = ( ( U ` a ) ` B ) )
13 12 sseq1d 
 |-  ( b = B -> ( ( ( U ` a ) ` b ) C_ ( TC ` a ) <-> ( ( U ` a ) ` B ) C_ ( TC ` a ) ) )
14 1 ituni0 
 |-  ( a e. _V -> ( ( U ` a ) ` (/) ) = a )
15 tcid 
 |-  ( a e. _V -> a C_ ( TC ` a ) )
16 14 15 eqsstrd 
 |-  ( a e. _V -> ( ( U ` a ) ` (/) ) C_ ( TC ` a ) )
17 16 elv 
 |-  ( ( U ` a ) ` (/) ) C_ ( TC ` a )
18 1 itunisuc 
 |-  ( ( U ` a ) ` suc c ) = U. ( ( U ` a ) ` c )
19 tctr 
 |-  Tr ( TC ` a )
20 pwtr 
 |-  ( Tr ( TC ` a ) <-> Tr ~P ( TC ` a ) )
21 19 20 mpbi 
 |-  Tr ~P ( TC ` a )
22 trss 
 |-  ( Tr ~P ( TC ` a ) -> ( ( ( U ` a ) ` c ) e. ~P ( TC ` a ) -> ( ( U ` a ) ` c ) C_ ~P ( TC ` a ) ) )
23 21 22 ax-mp 
 |-  ( ( ( U ` a ) ` c ) e. ~P ( TC ` a ) -> ( ( U ` a ) ` c ) C_ ~P ( TC ` a ) )
24 fvex 
 |-  ( ( U ` a ) ` c ) e. _V
25 24 elpw 
 |-  ( ( ( U ` a ) ` c ) e. ~P ( TC ` a ) <-> ( ( U ` a ) ` c ) C_ ( TC ` a ) )
26 sspwuni 
 |-  ( ( ( U ` a ) ` c ) C_ ~P ( TC ` a ) <-> U. ( ( U ` a ) ` c ) C_ ( TC ` a ) )
27 23 25 26 3imtr3i 
 |-  ( ( ( U ` a ) ` c ) C_ ( TC ` a ) -> U. ( ( U ` a ) ` c ) C_ ( TC ` a ) )
28 18 27 eqsstrid 
 |-  ( ( ( U ` a ) ` c ) C_ ( TC ` a ) -> ( ( U ` a ) ` suc c ) C_ ( TC ` a ) )
29 28 a1i 
 |-  ( c e. _om -> ( ( ( U ` a ) ` c ) C_ ( TC ` a ) -> ( ( U ` a ) ` suc c ) C_ ( TC ` a ) ) )
30 7 9 11 13 17 29 finds 
 |-  ( B e. _om -> ( ( U ` a ) ` B ) C_ ( TC ` a ) )
31 vex 
 |-  a e. _V
32 1 itunifn 
 |-  ( a e. _V -> ( U ` a ) Fn _om )
33 fndm 
 |-  ( ( U ` a ) Fn _om -> dom ( U ` a ) = _om )
34 31 32 33 mp2b 
 |-  dom ( U ` a ) = _om
35 34 eleq2i 
 |-  ( B e. dom ( U ` a ) <-> B e. _om )
36 ndmfv 
 |-  ( -. B e. dom ( U ` a ) -> ( ( U ` a ) ` B ) = (/) )
37 35 36 sylnbir 
 |-  ( -. B e. _om -> ( ( U ` a ) ` B ) = (/) )
38 0ss 
 |-  (/) C_ ( TC ` a )
39 37 38 eqsstrdi 
 |-  ( -. B e. _om -> ( ( U ` a ) ` B ) C_ ( TC ` a ) )
40 30 39 pm2.61i 
 |-  ( ( U ` a ) ` B ) C_ ( TC ` a )
41 5 40 vtoclg 
 |-  ( A e. _V -> ( ( U ` A ) ` B ) C_ ( TC ` A ) )
42 fv2prc 
 |-  ( -. A e. _V -> ( ( U ` A ) ` B ) = (/) )
43 0ss 
 |-  (/) C_ ( TC ` A )
44 42 43 eqsstrdi 
 |-  ( -. A e. _V -> ( ( U ` A ) ` B ) C_ ( TC ` A ) )
45 41 44 pm2.61i 
 |-  ( ( U ` A ) ` B ) C_ ( TC ` A )