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 𝑅