Metamath Proof Explorer

Definition df-bnj18

Description: Define the function giving: the transitive closure of X in A by R . 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 . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion df-bnj18 ⊢ trCl X A R = ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cX class X
1 cA class A
2 cR class R
3 1 2 0 c-bnj18 class trCl X A R
4 vf setvar f
5 vn setvar n
6 com class ω
7 c0 class ∅
8 7 csn class ∅
9 6 8 cdif class ω ∖ ∅
10 4 cv setvar f
11 5 cv setvar n
12 10 11 wfn wff f Fn n
13 7 10 cfv class f ⁡ ∅
14 1 2 0 c-bnj14 class pred X A R
15 13 14 wceq wff f ⁡ ∅ = pred X A R
16 vi setvar i
17 16 cv setvar i
18 17 csuc class suc ⁡ i
19 18 11 wcel wff suc ⁡ i ∈ n
20 18 10 cfv class f ⁡ suc ⁡ i
21 vy setvar y
22 17 10 cfv class f ⁡ i
23 21 cv setvar y
24 1 2 23 c-bnj14 class pred y A R
25 21 22 24 ciun class ⋃ y ∈ f ⁡ i pred y A R
26 20 25 wceq wff f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
27 19 26 wi wff suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
28 27 16 6 wral wff ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
29 12 15 28 w3a wff f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
30 29 5 9 wrex wff ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
31 30 4 cab class f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
32 10 cdm class dom ⁡ f
33 16 32 22 ciun class ⋃ i ∈ dom ⁡ f f ⁡ i
34 4 31 33 ciun class ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i
35 3 34 wceq wff trCl X A R = ⋃ f ∈ f | ∃ n ∈ ω ∖ ∅ f Fn n ∧ f ⁡ ∅ = pred X A R ∧ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R ⋃ i ∈ dom ⁡ f f ⁡ i