Definition df-bnj18 32236

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 32469. (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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3		cX	. . 3 class 𝑋
4	1, 2, 3	c-bnj18 32235	. 2 class trCl(𝑋, 𝐴, 𝑅)
5		vf	. . 3 setvar 𝑓
6	5	cv 1541	. . . . . . 7 class 𝑓
7		vn	. . . . . . . 8 setvar 𝑛
8	7	cv 1541	. . . . . . 7 class 𝑛
9	6, 8	wfn 6328	. . . . . 6 wff 𝑓 Fn 𝑛
10		c0 4209	. . . . . . . 8 class ∅
11	10, 6	cfv 6333	. . . . . . 7 class (𝑓‘∅)
12	1, 2, 3	c-bnj14 32229	. . . . . . 7 class pred(𝑋, 𝐴, 𝑅)
13	11, 12	wceq 1542	. . . . . 6 wff (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)
14		vi	. . . . . . . . . . 11 setvar 𝑖
15	14	cv 1541	. . . . . . . . . 10 class 𝑖
16	15	csuc 6168	. . . . . . . . 9 class suc 𝑖
17	16, 8	wcel 2113	. . . . . . . 8 wff suc 𝑖 ∈ 𝑛
18	16, 6	cfv 6333	. . . . . . . . 9 class (𝑓‘suc 𝑖)
19		vy	. . . . . . . . . 10 setvar 𝑦
20	15, 6	cfv 6333	. . . . . . . . . 10 class (𝑓‘𝑖)
21	19	cv 1541	. . . . . . . . . . 11 class 𝑦
22	1, 2, 21	c-bnj14 32229	. . . . . . . . . 10 class pred(𝑦, 𝐴, 𝑅)
23	19, 20, 22	ciun 4878	. . . . . . . . 9 class ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)
24	18, 23	wceq 1542	. . . . . . . 8 wff (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)
25	17, 24	wi 4	. . . . . . 7 wff (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))
26		com 7593	. . . . . . 7 class ω
27	25, 14, 26	wral 3053	. . . . . 6 wff ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))
28	9, 13, 27	w3a 1088	. . . . 5 wff (𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
29	10	csn 4513	. . . . . 6 class {∅}
30	26, 29	cdif 3838	. . . . 5 class (ω ∖ {∅})
31	28, 7, 30	wrex 3054	. . . 4 wff ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
32	31, 5	cab 2716	. . 3 class {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}
33	6	cdm 5519	. . . 4 class dom 𝑓
34	14, 33, 20	ciun 4878	. . 3 class ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
35	5, 32, 34	ciun 4878	. 2 class ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
36	4, 35	wceq 1542	1 wff trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)

This definition is referenced by:  bnj882  32469  bnj18eq1  32470