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 pwtr 
 |-  ( Tr ( R1 ` y ) <-> Tr ~P ( R1 ` y ) )
25 24 bilani 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> Tr ~P ( R1 ` y ) )
26 r1sucg 
 |-  ( y e. dom R1 -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
27 treq 
 |-  ( ( R1 ` suc y ) = ~P ( R1 ` y ) -> ( Tr ( R1 ` suc y ) <-> Tr ~P ( R1 ` y ) ) )
28 26 27 syl 
 |-  ( y e. dom R1 -> ( Tr ( R1 ` suc y ) <-> Tr ~P ( R1 ` y ) ) )
29 25 28 syl5ibrcom 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> ( y e. dom R1 -> Tr ( R1 ` suc y ) ) )
30 23 29 biimtrrid 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> ( suc y e. dom R1 -> Tr ( R1 ` suc y ) ) )
31 ndmfv 
 |-  ( -. suc y e. dom R1 -> ( R1 ` suc y ) = (/) )
32 treq 
 |-  ( ( R1 ` suc y ) = (/) -> ( Tr ( R1 ` suc y ) <-> Tr (/) ) )
33 31 32 syl 
 |-  ( -. suc y e. dom R1 -> ( Tr ( R1 ` suc y ) <-> Tr (/) ) )
34 21 33 mpbiri 
 |-  ( -. suc y e. dom R1 -> Tr ( R1 ` suc y ) )
35 30 34 pm2.61d1 
 |-  ( ( y e. On /\ Tr ( R1 ` y ) ) -> Tr ( R1 ` suc y ) )
36 35 ex 
 |-  ( y e. On -> ( Tr ( R1 ` y ) -> Tr ( R1 ` suc y ) ) )
37 triun 
 |-  ( A. y e. x Tr ( R1 ` y ) -> Tr U_ y e. x ( R1 ` y ) )
38 r1limg 
 |-  ( ( x e. dom R1 /\ Lim x ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
39 38 ancoms 
 |-  ( ( Lim x /\ x e. dom R1 ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
40 treq 
 |-  ( ( R1 ` x ) = U_ y e. x ( R1 ` y ) -> ( Tr ( R1 ` x ) <-> Tr U_ y e. x ( R1 ` y ) ) )
41 39 40 syl 
 |-  ( ( Lim x /\ x e. dom R1 ) -> ( Tr ( R1 ` x ) <-> Tr U_ y e. x ( R1 ` y ) ) )
42 37 41 imbitrrid 
 |-  ( ( Lim x /\ x e. dom R1 ) -> ( A. y e. x Tr ( R1 ` y ) -> Tr ( R1 ` x ) ) )
43 42 impancom 
 |-  ( ( Lim x /\ A. y e. x Tr ( R1 ` y ) ) -> ( x e. dom R1 -> Tr ( R1 ` x ) ) )
44 ndmfv 
 |-  ( -. x e. dom R1 -> ( R1 ` x ) = (/) )
45 44 10 syl 
 |-  ( -. x e. dom R1 -> ( Tr ( R1 ` x ) <-> Tr (/) ) )
46 21 45 mpbiri 
 |-  ( -. x e. dom R1 -> Tr ( R1 ` x ) )
47 43 46 pm2.61d1 
 |-  ( ( Lim x /\ A. y e. x Tr ( R1 ` y ) ) -> Tr ( R1 ` x ) )
48 47 ex 
 |-  ( Lim x -> ( A. y e. x Tr ( R1 ` y ) -> Tr ( R1 ` x ) ) )
49 11 14 17 20 21 36 48 tfinds 
 |-  ( A e. On -> Tr ( R1 ` A ) )
50 6 49 syl 
 |-  ( A e. dom R1 -> Tr ( R1 ` A ) )
51 ndmfv 
 |-  ( -. A e. dom R1 -> ( R1 ` A ) = (/) )
52 treq 
 |-  ( ( R1 ` A ) = (/) -> ( Tr ( R1 ` A ) <-> Tr (/) ) )
53 51 52 syl 
 |-  ( -. A e. dom R1 -> ( Tr ( R1 ` A ) <-> Tr (/) ) )
54 21 53 mpbiri 
 |-  ( -. A e. dom R1 -> Tr ( R1 ` A ) )
55 50 54 pm2.61i 
 |-  Tr ( R1 ` A )