Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnj18 Structured version   Visualization version   GIF version

Definition df-bnj18 30889
Description: Define the function giving: the transitive closure of 𝑋 in 𝐴 by 𝑅. This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 31122. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
df-bnj18 trCl(𝑋, 𝐴, 𝑅) = 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
Distinct variable groups:   𝑓,𝑋,𝑛,𝑖,𝑦   𝐴,𝑓,𝑛,𝑖,𝑦   𝑅,𝑓,𝑛,𝑖,𝑦

Detailed syntax breakdown of Definition df-bnj18
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
3 cX . . 3 class 𝑋
41, 2, 3c-bnj18 30888 . 2 class trCl(𝑋, 𝐴, 𝑅)
5 vf . . 3 setvar 𝑓
65cv 1522 . . . . . . 7 class 𝑓
7 vn . . . . . . . 8 setvar 𝑛
87cv 1522 . . . . . . 7 class 𝑛
96, 8wfn 5921 . . . . . 6 wff 𝑓 Fn 𝑛
10 c0 3948 . . . . . . . 8 class
1110, 6cfv 5926 . . . . . . 7 class (𝑓‘∅)
121, 2, 3c-bnj14 30882 . . . . . . 7 class pred(𝑋, 𝐴, 𝑅)
1311, 12wceq 1523 . . . . . 6 wff (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)
14 vi . . . . . . . . . . 11 setvar 𝑖
1514cv 1522 . . . . . . . . . 10 class 𝑖
1615csuc 5763 . . . . . . . . 9 class suc 𝑖
1716, 8wcel 2030 . . . . . . . 8 wff suc 𝑖𝑛
1816, 6cfv 5926 . . . . . . . . 9 class (𝑓‘suc 𝑖)
19 vy . . . . . . . . . 10 setvar 𝑦
2015, 6cfv 5926 . . . . . . . . . 10 class (𝑓𝑖)
2119cv 1522 . . . . . . . . . . 11 class 𝑦
221, 2, 21c-bnj14 30882 . . . . . . . . . 10 class pred(𝑦, 𝐴, 𝑅)
2319, 20, 22ciun 4552 . . . . . . . . 9 class 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)
2418, 23wceq 1523 . . . . . . . 8 wff (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)
2517, 24wi 4 . . . . . . 7 wff (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))
26 com 7107 . . . . . . 7 class ω
2725, 14, 26wral 2941 . . . . . 6 wff 𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))
289, 13, 27w3a 1054 . . . . 5 wff (𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
2910csn 4210 . . . . . 6 class {∅}
3026, 29cdif 3604 . . . . 5 class (ω ∖ {∅})
3128, 7, 30wrex 2942 . . . 4 wff 𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
3231, 5cab 2637 . . 3 class {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}
336cdm 5143 . . . 4 class dom 𝑓
3414, 33, 20ciun 4552 . . 3 class 𝑖 ∈ dom 𝑓(𝑓𝑖)
355, 32, 34ciun 4552 . 2 class 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
364, 35wceq 1523 1 wff trCl(𝑋, 𝐴, 𝑅) = 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
Colors of variables: wff setvar class
This definition is referenced by:  bnj882  31122  bnj18eq1  31123
  Copyright terms: Public domain W3C validator