Metamath Proof Explorer

Theorem r1tr

Description: The cumulative hierarchy of sets is transitive. Lemma 7T of Enderton p. 202. (Contributed by NM, 8-Sep-2003) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1tr 
|- Tr ( R1 ` A )

Proof

Step Hyp Ref Expression
1 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
2 1 simpri 
 |-  Lim dom R1
3 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
4 ordsson 
 |-  ( Ord dom R1 -> dom R1 C_ On )
5 2 3 4 mp2b 
 |-  dom R1 C_ On
6 5 sseli 
 |-  ( A e. dom R1 -> A e. On )
7 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
8 r10 
 |-  ( R1 ` (/) ) = (/)
9 7 8 eqtrdi 
 |-  ( x = (/) -> ( R1 ` x ) = (/) )
10 treq 
 |-  ( ( R1 ` x ) = (/) -> ( Tr ( R1 ` x ) <-> Tr (/) ) )
11 9 10 syl 
 |-  ( x = (/) -> ( Tr ( R1 ` x ) <-> Tr (/) ) )
12 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
13 treq 
 |-  ( ( R1 ` x ) = ( R1 ` y ) -> ( Tr ( R1 ` x ) <-> Tr ( R1 ` y ) ) )
14 12 13 syl 
 |-  ( x = y -> ( Tr ( R1 ` x ) <-> Tr ( R1 ` y ) ) )
15 fveq2 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
16 treq 
 |-  ( ( R1 ` x ) = ( R1 ` suc y ) -> ( Tr ( R1 ` x ) <-> Tr ( R1 ` suc y ) ) )
17 15 16 syl 
 |-  ( x = suc y -> ( Tr ( R1 ` x ) <-> Tr ( R1 ` suc y ) ) )
18 fveq2 
 |-  ( x = A -> ( R1 ` x ) = ( R1 ` A ) )
19 treq 
 |-  ( ( R1 ` x ) = ( R1 ` A ) -> ( Tr ( R1 ` x ) <-> Tr ( R1 ` A ) ) )
20 18 19 syl 
 |-  ( x = A -> ( Tr ( R1 ` x ) <-> Tr ( R1 ` A ) ) )
21 tr0 
 |-  Tr (/)
22 limsuc 
 |-  ( Lim dom R1 -> ( y e. dom R1 <-> suc y e. dom R1 ) )
23 2 22 ax-mp 
 |-  ( y e. dom R1 <-> suc y e. dom R1 )
24 simpr 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> Tr ( R1 ` y ) )
25 pwtr 
 |-  ( Tr ( R1 ` y ) <-> Tr ~P ( R1 ` y ) )
26 24 25 sylib 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> Tr ~P ( R1 ` y ) )
27 r1sucg 
 |-  ( y e. dom R1 -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
28 treq 
 |-  ( ( R1 ` suc y ) = ~P ( R1 ` y ) -> ( Tr ( R1 ` suc y ) <-> Tr ~P ( R1 ` y ) ) )
29 27 28 syl 
 |-  ( y e. dom R1 -> ( Tr ( R1 ` suc y ) <-> Tr ~P ( R1 ` y ) ) )
30 26 29 syl5ibrcom 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> ( y e. dom R1 -> Tr ( R1 ` suc y ) ) )
31 23 30 syl5bir 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> ( suc y e. dom R1 -> Tr ( R1 ` suc y ) ) )
32 ndmfv 
 |-  ( -. suc y e. dom R1 -> ( R1 ` suc y ) = (/) )
33 treq 
 |-  ( ( R1 ` suc y ) = (/) -> ( Tr ( R1 ` suc y ) <-> Tr (/) ) )
34 32 33 syl 
 |-  ( -. suc y e. dom R1 -> ( Tr ( R1 ` suc y ) <-> Tr (/) ) )
35 21 34 mpbiri 
 |-  ( -. suc y e. dom R1 -> Tr ( R1 ` suc y ) )
36 31 35 pm2.61d1 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> Tr ( R1 ` suc y ) )
37 36 ex 
 |-  ( y e. On -> ( Tr ( R1 ` y ) -> Tr ( R1 ` suc y ) ) )
38 triun 
 |-  ( A. y e. x Tr ( R1 ` y ) -> Tr U_ y e. x ( R1 ` y ) )
39 r1limg 
 |-  ( ( x e. dom R1 /\ Lim x ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
40 39 ancoms 
 |-  ( ( Lim x /\ x e. dom R1 ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
41 treq 
 |-  ( ( R1 ` x ) = U_ y e. x ( R1 ` y ) -> ( Tr ( R1 ` x ) <-> Tr U_ y e. x ( R1 ` y ) ) )
42 40 41 syl 
 |-  ( ( Lim x /\ x e. dom R1 ) -> ( Tr ( R1 ` x ) <-> Tr U_ y e. x ( R1 ` y ) ) )
43 38 42 syl5ibr 
 |-  ( ( Lim x /\ x e. dom R1 ) -> ( A. y e. x Tr ( R1 ` y ) -> Tr ( R1 ` x ) ) )
44 43 impancom 
 |-  ( ( Lim x /\ A. y e. x Tr ( R1 ` y ) ) -> ( x e. dom R1 -> Tr ( R1 ` x ) ) )
45 ndmfv 
 |-  ( -. x e. dom R1 -> ( R1 ` x ) = (/) )
46 45 10 syl 
 |-  ( -. x e. dom R1 -> ( Tr ( R1 ` x ) <-> Tr (/) ) )
47 21 46 mpbiri 
 |-  ( -. x e. dom R1 -> Tr ( R1 ` x ) )
48 44 47 pm2.61d1 
 |-  ( ( Lim x /\ A. y e. x Tr ( R1 ` y ) ) -> Tr ( R1 ` x ) )
49 48 ex 
 |-  ( Lim x -> ( A. y e. x Tr ( R1 ` y ) -> Tr ( R1 ` x ) ) )
50 11 14 17 20 21 37 49 tfinds 
 |-  ( A e. On -> Tr ( R1 ` A ) )
51 6 50 syl 
 |-  ( A e. dom R1 -> Tr ( R1 ` A ) )
52 ndmfv 
 |-  ( -. A e. dom R1 -> ( R1 ` A ) = (/) )
53 treq 
 |-  ( ( R1 ` A ) = (/) -> ( Tr ( R1 ` A ) <-> Tr (/) ) )
54 52 53 syl 
 |-  ( -. A e. dom R1 -> ( Tr ( R1 ` A ) <-> Tr (/) ) )
55 21 54 mpbiri 
 |-  ( -. A e. dom R1 -> Tr ( R1 ` A ) )
56 51 55 pm2.61i 
 |-  Tr ( R1 ` A )