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 𝑓(𝑓‘𝑖) |