Metamath Proof Explorer

Theorem itunitc

Description: The union of all union iterates creates the transitive closure; compare trcl . (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 itunitc 
|- ( TC ` A ) = U. ran ( U ` 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 -> ( TC ` a ) = ( TC ` A ) )
3 fveq2 
 |-  ( a = A -> ( U ` a ) = ( U ` A ) )
4 3 rneqd 
 |-  ( a = A -> ran ( U ` a ) = ran ( U ` A ) )
5 4 unieqd 
 |-  ( a = A -> U. ran ( U ` a ) = U. ran ( U ` A ) )
6 2 5 eqeq12d 
 |-  ( a = A -> ( ( TC ` a ) = U. ran ( U ` a ) <-> ( TC ` A ) = U. ran ( U ` A ) ) )
7 1 ituni0 
 |-  ( a e. _V -> ( ( U ` a ) ` (/) ) = a )
8 7 elv 
 |-  ( ( U ` a ) ` (/) ) = a
9 fvssunirn 
 |-  ( ( U ` a ) ` (/) ) C_ U. ran ( U ` a )
10 8 9 eqsstrri 
 |-  a C_ U. ran ( U ` a )
11 dftr3 
 |-  ( Tr U. ran ( U ` a ) <-> A. b e. U. ran ( U ` a ) b C_ U. ran ( U ` a ) )
12 vex 
 |-  a e. _V
13 1 itunifn 
 |-  ( a e. _V -> ( U ` a ) Fn _om )
14 fnunirn 
 |-  ( ( U ` a ) Fn _om -> ( b e. U. ran ( U ` a ) <-> E. c e. _om b e. ( ( U ` a ) ` c ) ) )
15 12 13 14 mp2b 
 |-  ( b e. U. ran ( U ` a ) <-> E. c e. _om b e. ( ( U ` a ) ` c ) )
16 elssuni 
 |-  ( b e. ( ( U ` a ) ` c ) -> b C_ U. ( ( U ` a ) ` c ) )
17 1 itunisuc 
 |-  ( ( U ` a ) ` suc c ) = U. ( ( U ` a ) ` c )
18 fvssunirn 
 |-  ( ( U ` a ) ` suc c ) C_ U. ran ( U ` a )
19 17 18 eqsstrri 
 |-  U. ( ( U ` a ) ` c ) C_ U. ran ( U ` a )
20 16 19 sstrdi 
 |-  ( b e. ( ( U ` a ) ` c ) -> b C_ U. ran ( U ` a ) )
21 20 rexlimivw 
 |-  ( E. c e. _om b e. ( ( U ` a ) ` c ) -> b C_ U. ran ( U ` a ) )
22 15 21 sylbi 
 |-  ( b e. U. ran ( U ` a ) -> b C_ U. ran ( U ` a ) )
23 11 22 mprgbir 
 |-  Tr U. ran ( U ` a )
24 tcmin 
 |-  ( a e. _V -> ( ( a C_ U. ran ( U ` a ) /\ Tr U. ran ( U ` a ) ) -> ( TC ` a ) C_ U. ran ( U ` a ) ) )
25 24 elv 
 |-  ( ( a C_ U. ran ( U ` a ) /\ Tr U. ran ( U ` a ) ) -> ( TC ` a ) C_ U. ran ( U ` a ) )
26 10 23 25 mp2an 
 |-  ( TC ` a ) C_ U. ran ( U ` a )
27 unissb 
 |-  ( U. ran ( U ` a ) C_ ( TC ` a ) <-> A. b e. ran ( U ` a ) b C_ ( TC ` a ) )
28 fvelrnb 
 |-  ( ( U ` a ) Fn _om -> ( b e. ran ( U ` a ) <-> E. c e. _om ( ( U ` a ) ` c ) = b ) )
29 12 13 28 mp2b 
 |-  ( b e. ran ( U ` a ) <-> E. c e. _om ( ( U ` a ) ` c ) = b )
30 1 itunitc1 
 |-  ( ( U ` a ) ` c ) C_ ( TC ` a )
31 30 a1i 
 |-  ( c e. _om -> ( ( U ` a ) ` c ) C_ ( TC ` a ) )
32 sseq1 
 |-  ( ( ( U ` a ) ` c ) = b -> ( ( ( U ` a ) ` c ) C_ ( TC ` a ) <-> b C_ ( TC ` a ) ) )
33 31 32 syl5ibcom 
 |-  ( c e. _om -> ( ( ( U ` a ) ` c ) = b -> b C_ ( TC ` a ) ) )
34 33 rexlimiv 
 |-  ( E. c e. _om ( ( U ` a ) ` c ) = b -> b C_ ( TC ` a ) )
35 29 34 sylbi 
 |-  ( b e. ran ( U ` a ) -> b C_ ( TC ` a ) )
36 27 35 mprgbir 
 |-  U. ran ( U ` a ) C_ ( TC ` a )
37 26 36 eqssi 
 |-  ( TC ` a ) = U. ran ( U ` a )
38 6 37 vtoclg 
 |-  ( A e. _V -> ( TC ` A ) = U. ran ( U ` A ) )
39 rn0 
 |-  ran (/) = (/)
40 39 unieqi 
 |-  U. ran (/) = U. (/)
41 uni0 
 |-  U. (/) = (/)
42 40 41 eqtr2i 
 |-  (/) = U. ran (/)
43 fvprc 
 |-  ( -. A e. _V -> ( TC ` A ) = (/) )
44 fvprc 
 |-  ( -. A e. _V -> ( U ` A ) = (/) )
45 44 rneqd 
 |-  ( -. A e. _V -> ran ( U ` A ) = ran (/) )
46 45 unieqd 
 |-  ( -. A e. _V -> U. ran ( U ` A ) = U. ran (/) )
47 42 43 46 3eqtr4a 
 |-  ( -. A e. _V -> ( TC ` A ) = U. ran ( U ` A ) )
48 38 47 pm2.61i 
 |-  ( TC ` A ) = U. ran ( U ` A )