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 ( 𝑅1𝐴 )

Proof

Step Hyp Ref Expression
1 r1funlim ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
2 1 simpri Lim dom 𝑅1
3 limord ( Lim dom 𝑅1 → Ord dom 𝑅1 )
4 ordsson ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
5 2 3 4 mp2b dom 𝑅1 ⊆ On
6 5 sseli ( 𝐴 ∈ dom 𝑅1𝐴 ∈ On )
7 fveq2 ( 𝑥 = ∅ → ( 𝑅1𝑥 ) = ( 𝑅1 ‘ ∅ ) )
8 r10 ( 𝑅1 ‘ ∅ ) = ∅
9 7 8 eqtrdi ( 𝑥 = ∅ → ( 𝑅1𝑥 ) = ∅ )
10 treq ( ( 𝑅1𝑥 ) = ∅ → ( Tr ( 𝑅1𝑥 ) ↔ Tr ∅ ) )
11 9 10 syl ( 𝑥 = ∅ → ( Tr ( 𝑅1𝑥 ) ↔ Tr ∅ ) )
12 fveq2 ( 𝑥 = 𝑦 → ( 𝑅1𝑥 ) = ( 𝑅1𝑦 ) )
13 treq ( ( 𝑅1𝑥 ) = ( 𝑅1𝑦 ) → ( Tr ( 𝑅1𝑥 ) ↔ Tr ( 𝑅1𝑦 ) ) )
14 12 13 syl ( 𝑥 = 𝑦 → ( Tr ( 𝑅1𝑥 ) ↔ Tr ( 𝑅1𝑦 ) ) )
15 fveq2 ( 𝑥 = suc 𝑦 → ( 𝑅1𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
16 treq ( ( 𝑅1𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) → ( Tr ( 𝑅1𝑥 ) ↔ Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
17 15 16 syl ( 𝑥 = suc 𝑦 → ( Tr ( 𝑅1𝑥 ) ↔ Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
18 fveq2 ( 𝑥 = 𝐴 → ( 𝑅1𝑥 ) = ( 𝑅1𝐴 ) )
19 treq ( ( 𝑅1𝑥 ) = ( 𝑅1𝐴 ) → ( Tr ( 𝑅1𝑥 ) ↔ Tr ( 𝑅1𝐴 ) ) )
20 18 19 syl ( 𝑥 = 𝐴 → ( Tr ( 𝑅1𝑥 ) ↔ Tr ( 𝑅1𝐴 ) ) )
21 tr0 Tr ∅
22 limsuc ( Lim dom 𝑅1 → ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 ) )
23 2 22 ax-mp ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 )
24 simpr ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1𝑦 ) ) → Tr ( 𝑅1𝑦 ) )
25 pwtr ( Tr ( 𝑅1𝑦 ) ↔ Tr 𝒫 ( 𝑅1𝑦 ) )
26 24 25 sylib ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1𝑦 ) ) → Tr 𝒫 ( 𝑅1𝑦 ) )
27 r1sucg ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1𝑦 ) )
28 treq ( ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1𝑦 ) → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr 𝒫 ( 𝑅1𝑦 ) ) )
29 27 28 syl ( 𝑦 ∈ dom 𝑅1 → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr 𝒫 ( 𝑅1𝑦 ) ) )
30 26 29 syl5ibrcom ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1𝑦 ) ) → ( 𝑦 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
31 23 30 syl5bir ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1𝑦 ) ) → ( suc 𝑦 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
32 ndmfv ( ¬ suc 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑦 ) = ∅ )
33 treq ( ( 𝑅1 ‘ suc 𝑦 ) = ∅ → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr ∅ ) )
34 32 33 syl ( ¬ suc 𝑦 ∈ dom 𝑅1 → ( Tr ( 𝑅1 ‘ suc 𝑦 ) ↔ Tr ∅ ) )
35 21 34 mpbiri ( ¬ suc 𝑦 ∈ dom 𝑅1 → Tr ( 𝑅1 ‘ suc 𝑦 ) )
36 31 35 pm2.61d1 ( ( 𝑦 ∈ On ∧ Tr ( 𝑅1𝑦 ) ) → Tr ( 𝑅1 ‘ suc 𝑦 ) )
37 36 ex ( 𝑦 ∈ On → ( Tr ( 𝑅1𝑦 ) → Tr ( 𝑅1 ‘ suc 𝑦 ) ) )
38 triun ( ∀ 𝑦𝑥 Tr ( 𝑅1𝑦 ) → Tr 𝑦𝑥 ( 𝑅1𝑦 ) )
39 r1limg ( ( 𝑥 ∈ dom 𝑅1 ∧ Lim 𝑥 ) → ( 𝑅1𝑥 ) = 𝑦𝑥 ( 𝑅1𝑦 ) )
40 39 ancoms ( ( Lim 𝑥𝑥 ∈ dom 𝑅1 ) → ( 𝑅1𝑥 ) = 𝑦𝑥 ( 𝑅1𝑦 ) )
41 treq ( ( 𝑅1𝑥 ) = 𝑦𝑥 ( 𝑅1𝑦 ) → ( Tr ( 𝑅1𝑥 ) ↔ Tr 𝑦𝑥 ( 𝑅1𝑦 ) ) )
42 40 41 syl ( ( Lim 𝑥𝑥 ∈ dom 𝑅1 ) → ( Tr ( 𝑅1𝑥 ) ↔ Tr 𝑦𝑥 ( 𝑅1𝑦 ) ) )
43 38 42 syl5ibr ( ( Lim 𝑥𝑥 ∈ dom 𝑅1 ) → ( ∀ 𝑦𝑥 Tr ( 𝑅1𝑦 ) → Tr ( 𝑅1𝑥 ) ) )
44 43 impancom ( ( Lim 𝑥 ∧ ∀ 𝑦𝑥 Tr ( 𝑅1𝑦 ) ) → ( 𝑥 ∈ dom 𝑅1 → Tr ( 𝑅1𝑥 ) ) )
45 ndmfv ( ¬ 𝑥 ∈ dom 𝑅1 → ( 𝑅1𝑥 ) = ∅ )
46 45 10 syl ( ¬ 𝑥 ∈ dom 𝑅1 → ( Tr ( 𝑅1𝑥 ) ↔ Tr ∅ ) )
47 21 46 mpbiri ( ¬ 𝑥 ∈ dom 𝑅1 → Tr ( 𝑅1𝑥 ) )
48 44 47 pm2.61d1 ( ( Lim 𝑥 ∧ ∀ 𝑦𝑥 Tr ( 𝑅1𝑦 ) ) → Tr ( 𝑅1𝑥 ) )
49 48 ex ( Lim 𝑥 → ( ∀ 𝑦𝑥 Tr ( 𝑅1𝑦 ) → Tr ( 𝑅1𝑥 ) ) )
50 11 14 17 20 21 37 49 tfinds ( 𝐴 ∈ On → Tr ( 𝑅1𝐴 ) )
51 6 50 syl ( 𝐴 ∈ dom 𝑅1 → Tr ( 𝑅1𝐴 ) )
52 ndmfv ( ¬ 𝐴 ∈ dom 𝑅1 → ( 𝑅1𝐴 ) = ∅ )
53 treq ( ( 𝑅1𝐴 ) = ∅ → ( Tr ( 𝑅1𝐴 ) ↔ Tr ∅ ) )
54 52 53 syl ( ¬ 𝐴 ∈ dom 𝑅1 → ( Tr ( 𝑅1𝐴 ) ↔ Tr ∅ ) )
55 21 54 mpbiri ( ¬ 𝐴 ∈ dom 𝑅1 → Tr ( 𝑅1𝐴 ) )
56 51 55 pm2.61i Tr ( 𝑅1𝐴 )