Definition df-ttrcl

Description: Define the transitive closure of a class. This is the smallest relation containing R (or more precisely, the relation ` ( R |`_V ) induced by R ) and having the transitive property. Definition from Levy p. 59, who denotes it as R * and calls it the "ancestral" of R . (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Assertion	df-ttrcl	⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	cttrcl	⊢ t++ 𝑅
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4		vn	⊢ 𝑛
5		com	⊢ ω
6		c1o	⊢ 1o
7	5 6	cdif	⊢ ( ω ∖ 1o )
8		vf	⊢ 𝑓
9	8	cv	⊢ 𝑓
10	4	cv	⊢ 𝑛
11	10	csuc	⊢ suc 𝑛
12	9 11	wfn	⊢ 𝑓 Fn suc 𝑛
13		c0	⊢ ∅
14	13 9	cfv	⊢ ( 𝑓 ‘ ∅ )
15	2	cv	⊢ 𝑥
16	14 15	wceq	⊢ ( 𝑓 ‘ ∅ ) = 𝑥
17	10 9	cfv	⊢ ( 𝑓 ‘ 𝑛 )
18	3	cv	⊢ 𝑦
19	17 18	wceq	⊢ ( 𝑓 ‘ 𝑛 ) = 𝑦
20	16 19	wa	⊢ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 )
21		vm	⊢ 𝑚
22	21	cv	⊢ 𝑚
23	22 9	cfv	⊢ ( 𝑓 ‘ 𝑚 )
24	22	csuc	⊢ suc 𝑚
25	24 9	cfv	⊢ ( 𝑓 ‘ suc 𝑚 )
26	23 25 0	wbr	⊢ ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 )
27	26 21 10	wral	⊢ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 )
28	12 20 27	w3a	⊢ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) )
29	28 8	wex	⊢ ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) )
30	29 4 7	wrex	⊢ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) )
31	30 2 3	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }
32	1 31	wceq	⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }