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 29808
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 30044. (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 29807 . 2 class trCl(𝑋, 𝐴, 𝑅)
5 vf . . 3 setvar 𝑓
65cv 1474 . . . . . . 7 class 𝑓
7 vn . . . . . . . 8 setvar 𝑛
87cv 1474 . . . . . . 7 class 𝑛
96, 8wfn 5785 . . . . . 6 wff 𝑓 Fn 𝑛
10 c0 3874 . . . . . . . 8 class
1110, 6cfv 5790 . . . . . . 7 class (𝑓‘∅)
121, 2, 3c-bnj14 29801 . . . . . . 7 class pred(𝑋, 𝐴, 𝑅)
1311, 12wceq 1475 . . . . . 6 wff (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)
14 vi . . . . . . . . . . 11 setvar 𝑖
1514cv 1474 . . . . . . . . . 10 class 𝑖
1615csuc 5628 . . . . . . . . 9 class suc 𝑖
1716, 8wcel 1977 . . . . . . . 8 wff suc 𝑖𝑛
1816, 6cfv 5790 . . . . . . . . 9 class (𝑓‘suc 𝑖)
19 vy . . . . . . . . . 10 setvar 𝑦
2015, 6cfv 5790 . . . . . . . . . 10 class (𝑓𝑖)
2119cv 1474 . . . . . . . . . . 11 class 𝑦
221, 2, 21c-bnj14 29801 . . . . . . . . . 10 class pred(𝑦, 𝐴, 𝑅)
2319, 20, 22ciun 4450 . . . . . . . . 9 class 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)
2418, 23wceq 1475 . . . . . . . 8 wff (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)
2517, 24wi 4 . . . . . . 7 wff (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))
26 com 6935 . . . . . . 7 class ω
2725, 14, 26wral 2896 . . . . . 6 wff 𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))
289, 13, 27w3a 1031 . . . . 5 wff (𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
2910csn 4125 . . . . . 6 class {∅}
3026, 29cdif 3537 . . . . 5 class (ω ∖ {∅})
3128, 7, 30wrex 2897 . . . 4 wff 𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
3231, 5cab 2596 . . 3 class {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}
336cdm 5028 . . . 4 class dom 𝑓
3414, 33, 20ciun 4450 . . 3 class 𝑖 ∈ dom 𝑓(𝑓𝑖)
355, 32, 34ciun 4450 . 2 class 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
364, 35wceq 1475 1 wff trCl(𝑋, 𝐴, 𝑅) = 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
Colors of variables: wff setvar class
This definition is referenced by:  bnj882  30044  bnj18eq1  30045
  Copyright terms: Public domain W3C validator