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 32682 |
. 2
class
trCl(𝑋, 𝐴, 𝑅) |
5 | | vf |
. . 3
setvar 𝑓 |
6 | 5 | cv 1538 |
. . . . . . 7
class 𝑓 |
7 | | vn |
. . . . . . . 8
setvar 𝑛 |
8 | 7 | cv 1538 |
. . . . . . 7
class 𝑛 |
9 | 6, 8 | wfn 6432 |
. . . . . 6
wff 𝑓 Fn 𝑛 |
10 | | c0 4257 |
. . . . . . . 8
class
∅ |
11 | 10, 6 | cfv 6437 |
. . . . . . 7
class (𝑓‘∅) |
12 | 1, 2, 3 | c-bnj14 32676 |
. . . . . . 7
class
pred(𝑋, 𝐴, 𝑅) |
13 | 11, 12 | wceq 1539 |
. . . . . 6
wff (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) |
14 | | vi |
. . . . . . . . . . 11
setvar 𝑖 |
15 | 14 | cv 1538 |
. . . . . . . . . 10
class 𝑖 |
16 | 15 | csuc 6272 |
. . . . . . . . 9
class suc 𝑖 |
17 | 16, 8 | wcel 2107 |
. . . . . . . 8
wff suc 𝑖 ∈ 𝑛 |
18 | 16, 6 | cfv 6437 |
. . . . . . . . 9
class (𝑓‘suc 𝑖) |
19 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
20 | 15, 6 | cfv 6437 |
. . . . . . . . . 10
class (𝑓‘𝑖) |
21 | 19 | cv 1538 |
. . . . . . . . . . 11
class 𝑦 |
22 | 1, 2, 21 | c-bnj14 32676 |
. . . . . . . . . 10
class
pred(𝑦, 𝐴, 𝑅) |
23 | 19, 20, 22 | ciun 4925 |
. . . . . . . . 9
class ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) |
24 | 18, 23 | wceq 1539 |
. . . . . . . 8
wff (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) |
25 | 17, 24 | wi 4 |
. . . . . . 7
wff (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
26 | | com 7721 |
. . . . . . 7
class
ω |
27 | 25, 14, 26 | wral 3065 |
. . . . . 6
wff
∀𝑖 ∈
ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
28 | 9, 13, 27 | w3a 1086 |
. . . . 5
wff (𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
29 | 10 | csn 4562 |
. . . . . 6
class
{∅} |
30 | 26, 29 | cdif 3885 |
. . . . 5
class (ω
∖ {∅}) |
31 | 28, 7, 30 | wrex 3066 |
. . . 4
wff
∃𝑛 ∈
(ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
32 | 31, 5 | cab 2716 |
. . 3
class {𝑓 ∣ ∃𝑛 ∈ (ω ∖
{∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))} |
33 | 6 | cdm 5590 |
. . . 4
class dom 𝑓 |
34 | 14, 33, 20 | ciun 4925 |
. . 3
class ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖) |
35 | 5, 32, 34 | ciun 4925 |
. 2
class ∪ 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) |
36 | 4, 35 | wceq 1539 |
1
wff trCl(𝑋, 𝐴, 𝑅) = ∪
𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖
{∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))}∪
𝑖 ∈ dom 𝑓(𝑓‘𝑖) |