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

Metamath Proof Explorer

Theorem dmttrcl

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

Ref Expression
Assertion dmttrcl dom t++ 𝑅 = dom 𝑅

Proof

Step Hyp Ref Expression
1 df-ttrcl ⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
2 1 dmeqi ⊢ dom t++ 𝑅 = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
3 dmopab ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) } = { 𝑥 ∣ ∃ 𝑦 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
4 2 3 eqtri ⊢ dom t++ 𝑅 = { 𝑥 ∣ ∃ 𝑦 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
5 simpr2l ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∅ ) = 𝑥 )
6 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝑓 ‘ 𝑎 ) = ( 𝑓 ‘ ∅ ) )
7 suceq ⊢ ( 𝑎 = ∅ → suc 𝑎 = suc ∅ )
8 df-1o ⊢ 1o = suc ∅
9 7 8 eqtr4di ⊢ ( 𝑎 = ∅ → suc 𝑎 = 1o )
10 9 fveq2d ⊢ ( 𝑎 = ∅ → ( 𝑓 ‘ suc 𝑎 ) = ( 𝑓 ‘ 1o ) )
11 6 10 breq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) )
12 simpr3 ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
13 eldif ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) ↔ ( 𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o ) )
14 0ex ⊢ ∅ ∈ V
15 nnord ⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
16 ordelsuc ⊢ ( ( ∅ ∈ V ∧ Ord 𝑛 ) → ( ∅ ∈ 𝑛 ↔ suc ∅ ⊆ 𝑛 ) )
17 14 15 16 sylancr ⊢ ( 𝑛 ∈ ω → ( ∅ ∈ 𝑛 ↔ suc ∅ ⊆ 𝑛 ) )
18 8 sseq1i ⊢ ( 1o ⊆ 𝑛 ↔ suc ∅ ⊆ 𝑛 )
19 1on ⊢ 1o ∈ On
20 19 onordi ⊢ Ord 1o
21 ordtri1 ⊢ ( ( Ord 1o ∧ Ord 𝑛 ) → ( 1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o ) )
22 20 15 21 sylancr ⊢ ( 𝑛 ∈ ω → ( 1o ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o ) )
23 18 22 bitr3id ⊢ ( 𝑛 ∈ ω → ( suc ∅ ⊆ 𝑛 ↔ ¬ 𝑛 ∈ 1o ) )
24 17 23 bitr2d ⊢ ( 𝑛 ∈ ω → ( ¬ 𝑛 ∈ 1o ↔ ∅ ∈ 𝑛 ) )
25 24 biimpa ⊢ ( ( 𝑛 ∈ ω ∧ ¬ 𝑛 ∈ 1o ) → ∅ ∈ 𝑛 )
26 13 25 sylbi ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ∅ ∈ 𝑛 )
27 26 adantr ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ∅ ∈ 𝑛 )
28 11 12 27 rspcdva ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) )
29 5 28 eqbrtrrd ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → 𝑥 𝑅 ( 𝑓 ‘ 1o ) )
30 vex ⊢ 𝑥 ∈ V
31 fvex ⊢ ( 𝑓 ‘ 1o ) ∈ V
32 30 31 breldm ⊢ ( 𝑥 𝑅 ( 𝑓 ‘ 1o ) → 𝑥 ∈ dom 𝑅 )
33 29 32 syl ⊢ ( ( 𝑛 ∈ ( ω ∖ 1o ) ∧ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) → 𝑥 ∈ dom 𝑅 )
34 33 ex ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 ∈ dom 𝑅 ) )
35 34 exlimdv ⊢ ( 𝑛 ∈ ( ω ∖ 1o ) → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 ∈ dom 𝑅 ) )
36 35 rexlimiv ⊢ ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 ∈ dom 𝑅 )
37 36 exlimiv ⊢ ( ∃ 𝑦 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → 𝑥 ∈ dom 𝑅 )
38 37 abssi ⊢ { 𝑥 ∣ ∃ 𝑦 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) } ⊆ dom 𝑅
39 4 38 eqsstri ⊢ dom t++ 𝑅 ⊆ dom 𝑅
40 dmresv ⊢ dom ( 𝑅 ↾ V ) = dom 𝑅
41 relres ⊢ Rel ( 𝑅 ↾ V )
42 ssttrcl ⊢ ( Rel ( 𝑅 ↾ V ) → ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V ) )
43 41 42 ax-mp ⊢ ( 𝑅 ↾ V ) ⊆ t++ ( 𝑅 ↾ V )
44 ttrclresv ⊢ t++ ( 𝑅 ↾ V ) = t++ 𝑅
45 43 44 sseqtri ⊢ ( 𝑅 ↾ V ) ⊆ t++ 𝑅
46 dmss ⊢ ( ( 𝑅 ↾ V ) ⊆ t++ 𝑅 → dom ( 𝑅 ↾ V ) ⊆ dom t++ 𝑅 )
47 45 46 ax-mp ⊢ dom ( 𝑅 ↾ V ) ⊆ dom t++ 𝑅
48 40 47 eqsstrri ⊢ dom 𝑅 ⊆ dom t++ 𝑅
49 39 48 eqssi ⊢ dom t++ 𝑅 = dom 𝑅