Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ttrcl Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 cR . . 3 class 𝑅
21cttrcl 33503 . 2 class t++𝑅
3 vf . . . . . . . 8 setvar 𝑓
43cv 1542 . . . . . . 7 class 𝑓
5 vn . . . . . . . . 9 setvar 𝑛
65cv 1542 . . . . . . . 8 class 𝑛
76csuc 6212 . . . . . . 7 class suc 𝑛
84, 7wfn 6372 . . . . . 6 wff 𝑓 Fn suc 𝑛
9 c0 4234 . . . . . . . . 9 class
109, 4cfv 6377 . . . . . . . 8 class (𝑓‘∅)
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1542 . . . . . . . 8 class 𝑥
1310, 12wceq 1543 . . . . . . 7 wff (𝑓‘∅) = 𝑥
146, 4cfv 6377 . . . . . . . 8 class (𝑓𝑛)
15 vy . . . . . . . . 9 setvar 𝑦
1615cv 1542 . . . . . . . 8 class 𝑦
1714, 16wceq 1543 . . . . . . 7 wff (𝑓𝑛) = 𝑦
1813, 17wa 399 . . . . . 6 wff ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑦)
19 vm . . . . . . . . . 10 setvar 𝑚
2019cv 1542 . . . . . . . . 9 class 𝑚
2120, 4cfv 6377 . . . . . . . 8 class (𝑓𝑚)
2220csuc 6212 . . . . . . . . 9 class suc 𝑚
2322, 4cfv 6377 . . . . . . . 8 class (𝑓‘suc 𝑚)
2421, 23, 1wbr 5050 . . . . . . 7 wff (𝑓𝑚)𝑅(𝑓‘suc 𝑚)
2524, 19, 6wral 3058 . . . . . 6 wff 𝑚𝑛 (𝑓𝑚)𝑅(𝑓‘suc 𝑚)
268, 18, 25w3a 1089 . . . . 5 wff (𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑦) ∧ ∀𝑚𝑛 (𝑓𝑚)𝑅(𝑓‘suc 𝑚))
2726, 3wex 1787 . . . 4 wff 𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑦) ∧ ∀𝑚𝑛 (𝑓𝑚)𝑅(𝑓‘suc 𝑚))
28 com 7641 . . . . 5 class ω
29 c1o 8192 . . . . 5 class 1o
3028, 29cdif 3860 . . . 4 class (ω ∖ 1o)
3127, 5, 30wrex 3059 . . 3 wff 𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑦) ∧ ∀𝑚𝑛 (𝑓𝑚)𝑅(𝑓‘suc 𝑚))
3231, 11, 15copab 5112 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑦) ∧ ∀𝑚𝑛 (𝑓𝑚)𝑅(𝑓‘suc 𝑚))}
332, 32wceq 1543 1 wff t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓𝑛) = 𝑦) ∧ ∀𝑚𝑛 (𝑓𝑚)𝑅(𝑓‘suc 𝑚))}
Colors of variables: wff setvar class
This definition is referenced by:  ttrcleq  33505  nfttrcld  33506  relttrcl  33508  brttrcl  33509  ttrclresv  33513  dmttrcl  33517  rnttrcl  33518
  Copyright terms: Public domain W3C validator