Definition df-ttrcl 9466

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 9465	. 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 6268	. . . . . . 7 class suc 𝑛
8	4, 7	wfn 6428	. . . . . 6 wff 𝑓 Fn suc 𝑛
9		c0 4256	. . . . . . . . 9 class ∅
10	9, 4	cfv 6433	. . . . . . . 8 class (𝑓‘∅)
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1538	. . . . . . . 8 class 𝑥
13	10, 12	wceq 1539	. . . . . . 7 wff (𝑓‘∅) = 𝑥
14	6, 4	cfv 6433	. . . . . . . 8 class (𝑓‘𝑛)
15		vy	. . . . . . . . 9 setvar 𝑦
16	15	cv 1538	. . . . . . . 8 class 𝑦
17	14, 16	wceq 1539	. . . . . . 7 wff (𝑓‘𝑛) = 𝑦
18	13, 17	wa 396	. . . . . 6 wff ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦)
19		vm	. . . . . . . . . 10 setvar 𝑚
20	19	cv 1538	. . . . . . . . 9 class 𝑚
21	20, 4	cfv 6433	. . . . . . . 8 class (𝑓‘𝑚)
22	20	csuc 6268	. . . . . . . . 9 class suc 𝑚
23	22, 4	cfv 6433	. . . . . . . 8 class (𝑓‘suc 𝑚)
24	21, 23, 1	wbr 5074	. . . . . . 7 wff (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)
25	24, 19, 6	wral 3064	. . . . . 6 wff ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)
26	8, 18, 25	w3a 1086	. . . . 5 wff (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
27	26, 3	wex 1782	. . . 4 wff ∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
28		com 7712	. . . . 5 class ω
29		c1o 8290	. . . . 5 class 1o
30	28, 29	cdif 3884	. . . 4 class (ω ∖ 1o)
31	27, 5, 30	wrex 3065	. . 3 wff ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
32	31, 11, 15	copab 5136	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}
33	2, 32	wceq 1539	1 wff t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}

This definition is referenced by:  ttrcleq  9467  nfttrcld  9468  relttrcl  9470  brttrcl  9471  ttrclresv  9475  dmttrcl  9479  rnttrcl  9480