Definition df-ttrcl 33504

Description: Define the transitive closure of a class. This is the smallest relationship containing 𝑅 (or more precisely, the relation (𝑅 ↾ V) induced by 𝑅) and having the transitive property. Definition from [Levy] p. 59, who denotes it as 𝑅∗ and calls it the "ancestral" of 𝑅. (Contributed by Scott Fenton, 17-Oct-2024.)

Assertion

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

Distinct variable group:   𝑅,𝑓,𝑛,𝑚,𝑥,𝑦

Detailed syntax breakdown of Definition df-ttrcl

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	cttrcl 33503	. 2 class t++𝑅
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1542	. . . . . . 7 class 𝑓
5		vn	. . . . . . . . 9 setvar 𝑛
6	5	cv 1542	. . . . . . . 8 class 𝑛
7	6	csuc 6212	. . . . . . 7 class suc 𝑛
8	4, 7	wfn 6372	. . . . . 6 wff 𝑓 Fn suc 𝑛
9		c0 4234	. . . . . . . . 9 class ∅
10	9, 4	cfv 6377	. . . . . . . 8 class (𝑓‘∅)
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1542	. . . . . . . 8 class 𝑥
13	10, 12	wceq 1543	. . . . . . 7 wff (𝑓‘∅) = 𝑥
14	6, 4	cfv 6377	. . . . . . . 8 class (𝑓‘𝑛)
15		vy	. . . . . . . . 9 setvar 𝑦
16	15	cv 1542	. . . . . . . 8 class 𝑦
17	14, 16	wceq 1543	. . . . . . 7 wff (𝑓‘𝑛) = 𝑦
18	13, 17	wa 399	. . . . . 6 wff ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦)
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1542	. . . . . . . . 9 class 𝑚
21	20, 4	cfv 6377	. . . . . . . 8 class (𝑓‘𝑚)
22	20	csuc 6212	. . . . . . . . 9 class suc 𝑚
23	22, 4	cfv 6377	. . . . . . . 8 class (𝑓‘suc 𝑚)
24	21, 23, 1	wbr 5050	. . . . . . 7 wff (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)
25	24, 19, 6	wral 3058	. . . . . 6 wff ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)
26	8, 18, 25	w3a 1089	. . . . 5 wff (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
27	26, 3	wex 1787	. . . 4 wff ∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
28		com 7641	. . . . 5 class ω
29		c1o 8192	. . . . 5 class 1o
30	28, 29	cdif 3860	. . . 4 class (ω ∖ 1o)
31	27, 5, 30	wrex 3059	. . 3 wff ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
32	31, 11, 15	copab 5112	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}
33	2, 32	wceq 1543	1 wff t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}

This definition is referenced by:  ttrcleq  33505  nfttrcld  33506  relttrcl  33508  brttrcl  33509  ttrclresv  33513  dmttrcl  33517  rnttrcl  33518