Metamath Proof Explorer

Theorem r1tr

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