Metamath Proof Explorer

Theorem trcl

Description: For any set A , show the properties of its transitive closure C . Similar to Theorem 9.1 of TakeutiZaring p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 for an abbreviated version showing existence. (Contributed by NM, 14-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses trcl.1 
|- A e. _V
trcl.2 
|- F = ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om )
trcl.3 
|- C = U_ y e. _om ( F ` y )
Assertion trcl 
|- ( A C_ C /\ Tr C /\ A. x ( ( A C_ x /\ Tr x ) -> C C_ x ) )

Proof

Step Hyp Ref Expression
1 trcl.1 
 |-  A e. _V
2 trcl.2 
 |-  F = ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om )
3 trcl.3 
 |-  C = U_ y e. _om ( F ` y )
4 peano1 
 |-  (/) e. _om
5 2 fveq1i 
 |-  ( F ` (/) ) = ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` (/) )
6 fr0g 
 |-  ( A e. _V -> ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` (/) ) = A )
7 1 6 ax-mp 
 |-  ( ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` _om ) ` (/) ) = A
8 5 7 eqtr2i 
 |-  A = ( F ` (/) )
9 8 eqimssi 
 |-  A C_ ( F ` (/) )
10 fveq2 
 |-  ( y = (/) -> ( F ` y ) = ( F ` (/) ) )
11 10 sseq2d 
 |-  ( y = (/) -> ( A C_ ( F ` y ) <-> A C_ ( F ` (/) ) ) )
12 11 rspcev 
 |-  ( ( (/) e. _om /\ A C_ ( F ` (/) ) ) -> E. y e. _om A C_ ( F ` y ) )
13 4 9 12 mp2an 
 |-  E. y e. _om A C_ ( F ` y )
14 ssiun 
 |-  ( E. y e. _om A C_ ( F ` y ) -> A C_ U_ y e. _om ( F ` y ) )
15 13 14 ax-mp 
 |-  A C_ U_ y e. _om ( F ` y )
16 15 3 sseqtrri 
 |-  A C_ C
17 dftr2 
 |-  ( Tr U_ y e. _om ( F ` y ) <-> A. v A. u ( ( v e. u /\ u e. U_ y e. _om ( F ` y ) ) -> v e. U_ y e. _om ( F ` y ) ) )
18 eliun 
 |-  ( u e. U_ y e. _om ( F ` y ) <-> E. y e. _om u e. ( F ` y ) )
19 18 anbi2i 
 |-  ( ( v e. u /\ u e. U_ y e. _om ( F ` y ) ) <-> ( v e. u /\ E. y e. _om u e. ( F ` y ) ) )
20 r19.42v 
 |-  ( E. y e. _om ( v e. u /\ u e. ( F ` y ) ) <-> ( v e. u /\ E. y e. _om u e. ( F ` y ) ) )
21 19 20 bitr4i 
 |-  ( ( v e. u /\ u e. U_ y e. _om ( F ` y ) ) <-> E. y e. _om ( v e. u /\ u e. ( F ` y ) ) )
22 elunii 
 |-  ( ( v e. u /\ u e. ( F ` y ) ) -> v e. U. ( F ` y ) )
23 ssun2 
 |-  U. ( F ` y ) C_ ( ( F ` y ) u. U. ( F ` y ) )
24 fvex 
 |-  ( F ` y ) e. _V
25 24 uniex 
 |-  U. ( F ` y ) e. _V
26 24 25 unex 
 |-  ( ( F ` y ) u. U. ( F ` y ) ) e. _V
27 id 
 |-  ( x = z -> x = z )
28 unieq 
 |-  ( x = z -> U. x = U. z )
29 27 28 uneq12d 
 |-  ( x = z -> ( x u. U. x ) = ( z u. U. z ) )
30 id 
 |-  ( x = ( F ` y ) -> x = ( F ` y ) )
31 unieq 
 |-  ( x = ( F ` y ) -> U. x = U. ( F ` y ) )
32 30 31 uneq12d 
 |-  ( x = ( F ` y ) -> ( x u. U. x ) = ( ( F ` y ) u. U. ( F ` y ) ) )
33 2 29 32 frsucmpt2 
 |-  ( ( y e. _om /\ ( ( F ` y ) u. U. ( F ` y ) ) e. _V ) -> ( F ` suc y ) = ( ( F ` y ) u. U. ( F ` y ) ) )
34 26 33 mpan2 
 |-  ( y e. _om -> ( F ` suc y ) = ( ( F ` y ) u. U. ( F ` y ) ) )
35 23 34 sseqtrrid 
 |-  ( y e. _om -> U. ( F ` y ) C_ ( F ` suc y ) )
36 35 sseld 
 |-  ( y e. _om -> ( v e. U. ( F ` y ) -> v e. ( F ` suc y ) ) )
37 22 36 syl5 
 |-  ( y e. _om -> ( ( v e. u /\ u e. ( F ` y ) ) -> v e. ( F ` suc y ) ) )
38 37 reximia 
 |-  ( E. y e. _om ( v e. u /\ u e. ( F ` y ) ) -> E. y e. _om v e. ( F ` suc y ) )
39 21 38 sylbi 
 |-  ( ( v e. u /\ u e. U_ y e. _om ( F ` y ) ) -> E. y e. _om v e. ( F ` suc y ) )
40 peano2 
 |-  ( y e. _om -> suc y e. _om )
41 fveq2 
 |-  ( u = suc y -> ( F ` u ) = ( F ` suc y ) )
42 41 eleq2d 
 |-  ( u = suc y -> ( v e. ( F ` u ) <-> v e. ( F ` suc y ) ) )
43 42 rspcev 
 |-  ( ( suc y e. _om /\ v e. ( F ` suc y ) ) -> E. u e. _om v e. ( F ` u ) )
44 43 ex 
 |-  ( suc y e. _om -> ( v e. ( F ` suc y ) -> E. u e. _om v e. ( F ` u ) ) )
45 40 44 syl 
 |-  ( y e. _om -> ( v e. ( F ` suc y ) -> E. u e. _om v e. ( F ` u ) ) )
46 45 rexlimiv 
 |-  ( E. y e. _om v e. ( F ` suc y ) -> E. u e. _om v e. ( F ` u ) )
47 fveq2 
 |-  ( y = u -> ( F ` y ) = ( F ` u ) )
48 47 eleq2d 
 |-  ( y = u -> ( v e. ( F ` y ) <-> v e. ( F ` u ) ) )
49 48 cbvrexvw 
 |-  ( E. y e. _om v e. ( F ` y ) <-> E. u e. _om v e. ( F ` u ) )
50 46 49 sylibr 
 |-  ( E. y e. _om v e. ( F ` suc y ) -> E. y e. _om v e. ( F ` y ) )
51 eliun 
 |-  ( v e. U_ y e. _om ( F ` y ) <-> E. y e. _om v e. ( F ` y ) )
52 50 51 sylibr 
 |-  ( E. y e. _om v e. ( F ` suc y ) -> v e. U_ y e. _om ( F ` y ) )
53 39 52 syl 
 |-  ( ( v e. u /\ u e. U_ y e. _om ( F ` y ) ) -> v e. U_ y e. _om ( F ` y ) )
54 53 ax-gen 
 |-  A. u ( ( v e. u /\ u e. U_ y e. _om ( F ` y ) ) -> v e. U_ y e. _om ( F ` y ) )
55 17 54 mpgbir 
 |-  Tr U_ y e. _om ( F ` y )
56 treq 
 |-  ( C = U_ y e. _om ( F ` y ) -> ( Tr C <-> Tr U_ y e. _om ( F ` y ) ) )
57 3 56 ax-mp 
 |-  ( Tr C <-> Tr U_ y e. _om ( F ` y ) )
58 55 57 mpbir 
 |-  Tr C
59 fveq2 
 |-  ( v = (/) -> ( F ` v ) = ( F ` (/) ) )
60 59 sseq1d 
 |-  ( v = (/) -> ( ( F ` v ) C_ x <-> ( F ` (/) ) C_ x ) )
61 fveq2 
 |-  ( v = y -> ( F ` v ) = ( F ` y ) )
62 61 sseq1d 
 |-  ( v = y -> ( ( F ` v ) C_ x <-> ( F ` y ) C_ x ) )
63 fveq2 
 |-  ( v = suc y -> ( F ` v ) = ( F ` suc y ) )
64 63 sseq1d 
 |-  ( v = suc y -> ( ( F ` v ) C_ x <-> ( F ` suc y ) C_ x ) )
65 5 7 eqtri 
 |-  ( F ` (/) ) = A
66 65 sseq1i 
 |-  ( ( F ` (/) ) C_ x <-> A C_ x )
67 66 biimpri 
 |-  ( A C_ x -> ( F ` (/) ) C_ x )
68 67 adantr 
 |-  ( ( A C_ x /\ Tr x ) -> ( F ` (/) ) C_ x )
69 uniss 
 |-  ( ( F ` y ) C_ x -> U. ( F ` y ) C_ U. x )
70 df-tr 
 |-  ( Tr x <-> U. x C_ x )
71 sstr2 
 |-  ( U. ( F ` y ) C_ U. x -> ( U. x C_ x -> U. ( F ` y ) C_ x ) )
72 70 71 syl5bi 
 |-  ( U. ( F ` y ) C_ U. x -> ( Tr x -> U. ( F ` y ) C_ x ) )
73 69 72 syl 
 |-  ( ( F ` y ) C_ x -> ( Tr x -> U. ( F ` y ) C_ x ) )
74 73 anc2li 
 |-  ( ( F ` y ) C_ x -> ( Tr x -> ( ( F ` y ) C_ x /\ U. ( F ` y ) C_ x ) ) )
75 unss 
 |-  ( ( ( F ` y ) C_ x /\ U. ( F ` y ) C_ x ) <-> ( ( F ` y ) u. U. ( F ` y ) ) C_ x )
76 74 75 syl6ib 
 |-  ( ( F ` y ) C_ x -> ( Tr x -> ( ( F ` y ) u. U. ( F ` y ) ) C_ x ) )
77 34 sseq1d 
 |-  ( y e. _om -> ( ( F ` suc y ) C_ x <-> ( ( F ` y ) u. U. ( F ` y ) ) C_ x ) )
78 77 biimprd 
 |-  ( y e. _om -> ( ( ( F ` y ) u. U. ( F ` y ) ) C_ x -> ( F ` suc y ) C_ x ) )
79 76 78 syl9r 
 |-  ( y e. _om -> ( ( F ` y ) C_ x -> ( Tr x -> ( F ` suc y ) C_ x ) ) )
80 79 com23 
 |-  ( y e. _om -> ( Tr x -> ( ( F ` y ) C_ x -> ( F ` suc y ) C_ x ) ) )
81 80 adantld 
 |-  ( y e. _om -> ( ( A C_ x /\ Tr x ) -> ( ( F ` y ) C_ x -> ( F ` suc y ) C_ x ) ) )
82 60 62 64 68 81 finds2 
 |-  ( v e. _om -> ( ( A C_ x /\ Tr x ) -> ( F ` v ) C_ x ) )
83 82 com12 
 |-  ( ( A C_ x /\ Tr x ) -> ( v e. _om -> ( F ` v ) C_ x ) )
84 83 ralrimiv 
 |-  ( ( A C_ x /\ Tr x ) -> A. v e. _om ( F ` v ) C_ x )
85 fveq2 
 |-  ( y = v -> ( F ` y ) = ( F ` v ) )
86 85 cbviunv 
 |-  U_ y e. _om ( F ` y ) = U_ v e. _om ( F ` v )
87 3 86 eqtri 
 |-  C = U_ v e. _om ( F ` v )
88 87 sseq1i 
 |-  ( C C_ x <-> U_ v e. _om ( F ` v ) C_ x )
89 iunss 
 |-  ( U_ v e. _om ( F ` v ) C_ x <-> A. v e. _om ( F ` v ) C_ x )
90 88 89 bitri 
 |-  ( C C_ x <-> A. v e. _om ( F ` v ) C_ x )
91 84 90 sylibr 
 |-  ( ( A C_ x /\ Tr x ) -> C C_ x )
92 91 ax-gen 
 |-  A. x ( ( A C_ x /\ Tr x ) -> C C_ x )
93 16 58 92 3pm3.2i 
 |-  ( A C_ C /\ Tr C /\ A. x ( ( A C_ x /\ Tr x ) -> C C_ x ) )