Definition df-ttrcl 33694

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 33693	. 2 class t++𝑅
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1538	. . . . . . 7 class 𝑓
5		vn	. . . . . . . . 9 setvar 𝑛
6	5	cv 1538	. . . . . . . 8 class 𝑛
7	6	csuc 6253	. . . . . . 7 class suc 𝑛
8	4, 7	wfn 6413	. . . . . 6 wff 𝑓 Fn suc 𝑛
9		c0 4253	. . . . . . . . 9 class ∅
10	9, 4	cfv 6418	. . . . . . . 8 class (𝑓‘∅)
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1538	. . . . . . . 8 class 𝑥
13	10, 12	wceq 1539	. . . . . . 7 wff (𝑓‘∅) = 𝑥
14	6, 4	cfv 6418	. . . . . . . 8 class (𝑓‘𝑛)
15		vy	. . . . . . . . 9 setvar 𝑦
16	15	cv 1538	. . . . . . . 8 class 𝑦
17	14, 16	wceq 1539	. . . . . . 7 wff (𝑓‘𝑛) = 𝑦
18	13, 17	wa 395	. . . . . 6 wff ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦)
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1538	. . . . . . . . 9 class 𝑚
21	20, 4	cfv 6418	. . . . . . . 8 class (𝑓‘𝑚)
22	20	csuc 6253	. . . . . . . . 9 class suc 𝑚
23	22, 4	cfv 6418	. . . . . . . 8 class (𝑓‘suc 𝑚)
24	21, 23, 1	wbr 5070	. . . . . . 7 wff (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)
25	24, 19, 6	wral 3063	. . . . . 6 wff ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)
26	8, 18, 25	w3a 1085	. . . . 5 wff (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
27	26, 3	wex 1783	. . . 4 wff ∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
28		com 7687	. . . . 5 class ω
29		c1o 8260	. . . . 5 class 1o
30	28, 29	cdif 3880	. . . 4 class (ω ∖ 1o)
31	27, 5, 30	wrex 3064	. . 3 wff ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
32	31, 11, 15	copab 5132	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}
33	2, 32	wceq 1539	1 wff t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}

This definition is referenced by:  ttrcleq  33695  nfttrcld  33696  relttrcl  33698  brttrcl  33699  ttrclresv  33703  dmttrcl  33707  rnttrcl  33708