This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnttrcl

Description: The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024)

Ref Expression
Assertion rnttrcl ran t++ 𝑅 = ran 𝑅

Proof

Step Hyp Ref Expression
1 df-ttrcl ⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
2 1 rneqi ⊢ ran t++ 𝑅 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
3 rnopab ⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) } = { 𝑦 ∣ ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
4 2 3 eqtri ⊢ ran t++ 𝑅 = { 𝑦 ∣ ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
5 fveq2 ⊢ ( 𝑎 = ∪ 𝑛 → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ ∪ 𝑛 ) )
6 suceq ⊢ ( 𝑎 = ∪ 𝑛 → suc 𝑎 = suc ∪ 𝑛 )
7 6 fveq2d ⊢ ( 𝑎 = ∪ 𝑛 → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ suc ∪ 𝑛 ) )
8 5 7 breq12d ⊢ ( 𝑎 = ∪ 𝑛 → ( ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 ( 𝑓 ‘ suc ∪ 𝑛 ) ) )
9 simpr3 ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
10 df-1o ⊢ 1o = suc ∅
11 10 difeq2i ⊢ ( ω ∖ 1o ) = ( ω ∖ suc ∅ )
12 11 eleq2i ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) ↔ 𝑛 ∈ ( ω ∖ suc ∅ ) )
13 peano1 ⊢ ∅ ∈ ω
14 eldifsucnn ⊢ ( ∅ ∈ ω → ( 𝑛 ∈ ( ω ∖ suc ∅ ) ↔ ∃ 𝑥 ∈ ( ω ∖ ∅ ) 𝑛 = suc 𝑥 ) )
15 13 14 ax-mp ⊢ ( 𝑛 ∈ ( ω ∖ suc ∅ ) ↔ ∃ 𝑥 ∈ ( ω ∖ ∅ ) 𝑛 = suc 𝑥 )
16 dif0 ⊢ ( ω ∖ ∅ ) = ω
17 16 rexeqi ⊢ ( ∃ 𝑥 ∈ ( ω ∖ ∅ ) 𝑛 = suc 𝑥 ↔ ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 )
18 12 15 17 3bitri ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) ↔ ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 )
19 nnord ⊢ ( 𝑥 ∈ ω → Ord 𝑥 )
20 ordunisuc ⊢ ( Ord 𝑥 → ∪ suc 𝑥 = 𝑥 )
21 19 20 syl ⊢ ( 𝑥 ∈ ω → ∪ suc 𝑥 = 𝑥 )
22 vex ⊢ 𝑥 ∈ V
23 22 sucid ⊢ 𝑥 ∈ suc 𝑥
24 21 23 eqeltrdi ⊢ ( 𝑥 ∈ ω → ∪ suc 𝑥 ∈ suc 𝑥 )
25 unieq ⊢ ( 𝑛 = suc 𝑥 → ∪ 𝑛 = ∪ suc 𝑥 )
26 id ⊢ ( 𝑛 = suc 𝑥 → 𝑛 = suc 𝑥 )
27 25 26 eleq12d ⊢ ( 𝑛 = suc 𝑥 → ( ∪ 𝑛 ∈ 𝑛 ↔ ∪ suc 𝑥 ∈ suc 𝑥 ) )
28 24 27 syl5ibrcom ⊢ ( 𝑥 ∈ ω → ( 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛 ) )
29 28 rexlimiv ⊢ ( ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 → ∪ 𝑛 ∈ 𝑛 )
30 18 29 sylbi ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ∪ 𝑛 ∈ 𝑛 )
31 30 adantr ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∪ 𝑛 ∈ 𝑛 )
32 8 9 31 rspcdva ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 ( 𝑓 ‘ suc ∪ 𝑛 ) )
33 suceq ⊢ ( ∪ suc 𝑥 = 𝑥 → suc ∪ suc 𝑥 = suc 𝑥 )
34 21 33 syl ⊢ ( 𝑥 ∈ ω → suc ∪ suc 𝑥 = suc 𝑥 )
35 suceq ⊢ ( ∪ 𝑛 = ∪ suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥 )
36 25 35 syl ⊢ ( 𝑛 = suc 𝑥 → suc ∪ 𝑛 = suc ∪ suc 𝑥 )
37 36 26 eqeq12d ⊢ ( 𝑛 = suc 𝑥 → ( suc ∪ 𝑛 = 𝑛 ↔ suc ∪ suc 𝑥 = suc 𝑥 ) )
38 34 37 syl5ibrcom ⊢ ( 𝑥 ∈ ω → ( 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛 ) )
39 38 rexlimiv ⊢ ( ∃ 𝑥 ∈ ω 𝑛 = suc 𝑥 → suc ∪ 𝑛 = 𝑛 )
40 18 39 sylbi ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → suc ∪ 𝑛 = 𝑛 )
41 40 fveq2d ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( 𝑓 ‘ suc ∪ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
42 41 adantr ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc ∪ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
43 simpr2r ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ 𝑛 ) = 𝑦 )
44 42 43 eqtrd ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ suc ∪ 𝑛 ) = 𝑦 )
45 32 44 breqtrd ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 𝑦 )
46 fvex ⊢ ( 𝑓 ‘ ∪ 𝑛 ) ∈ V
47 vex ⊢ 𝑦 ∈ V
48 46 47 brelrn ⊢ ( ( 𝑓 ‘ ∪ 𝑛 ) 𝑅 𝑦 → 𝑦 ∈ ran 𝑅 )
49 45 48 syl ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → 𝑦 ∈ ran 𝑅 )
50 49 ex ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 ) )
51 50 exlimdv ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 ) )
52 51 rexlimiv ⊢ ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 )
53 52 exlimiv ⊢ ( ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑦 ∈ ran 𝑅 )
54 53 abssi ⊢ { 𝑦 ∣ ∃ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) } ⊆ ran 𝑅
55 4 54 eqsstri ⊢ ran t++ 𝑅 ⊆ ran 𝑅
56 rnresv ⊢ ran ( 𝑅 ↾ V ) = ran 𝑅
57 relres ⊢ Rel ( 𝑅 ↾ V )
58 ssttrcl ⊢ ( Rel ( 𝑅 ↾ V ) → ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V ) )
59 57 58 ax-mp ⊢ ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V )
60 ttrclresv ⊢ t++ ( 𝑅 ↾ V ) = t++ 𝑅
61 59 60 sseqtri ⊢ ( 𝑅 ↾ V ) ⊆ t++ 𝑅
62 61 rnssi ⊢ ran ( 𝑅 ↾ V ) ⊆ ran t++ 𝑅
63 56 62 eqsstrri ⊢ ran 𝑅 ⊆ ran t++ 𝑅
64 55 63 eqssi ⊢ ran t++ 𝑅 = ran 𝑅