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 biimtrrid ⊢ ( ( 𝑦 ∈ 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 imbitrrid ⊢ ( ( 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 ‘ 𝐴 )