Metamath Proof Explorer

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++ R = x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 0 cttrcl class t++ R
2 vx setvar x
3 vy setvar y
4 vn setvar n
5 com class ω
6 c1o class 1 𝑜
7 5 6 cdif class ω ∖ 1 𝑜
8 vf setvar f
9 8 cv setvar f
10 4 cv setvar n
11 10 csuc class suc ⁡ n
12 9 11 wfn wff f Fn suc ⁡ n
13 c0 class ∅
14 13 9 cfv class f ⁡ ∅
15 2 cv setvar x
16 14 15 wceq wff f ⁡ ∅ = x
17 10 9 cfv class f ⁡ n
18 3 cv setvar y
19 17 18 wceq wff f ⁡ n = y
20 16 19 wa wff f ⁡ ∅ = x ∧ f ⁡ n = y
21 vm setvar m
22 21 cv setvar m
23 22 9 cfv class f ⁡ m
24 22 csuc class suc ⁡ m
25 24 9 cfv class f ⁡ suc ⁡ m
26 23 25 0 wbr wff f ⁡ m R f ⁡ suc ⁡ m
27 26 21 10 wral wff ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m
28 12 20 27 w3a wff f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m
29 28 8 wex wff ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m
30 29 4 7 wrex wff ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m
31 30 2 3 copab class x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m
32 1 31 wceq wff t++ R = x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m