Step | Hyp | Ref
| Expression |
1 | | cwina 10626 |
. 2
class
Inaccw |
2 | | vx |
. . . . . 6
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . 5
class 𝑥 |
4 | | c0 4286 |
. . . . 5
class
∅ |
5 | 3, 4 | wne 2940 |
. . . 4
wff 𝑥 ≠ ∅ |
6 | | ccf 9881 |
. . . . . 6
class
cf |
7 | 3, 6 | cfv 6500 |
. . . . 5
class
(cf‘𝑥) |
8 | 7, 3 | wceq 1542 |
. . . 4
wff
(cf‘𝑥) = 𝑥 |
9 | | vy |
. . . . . . . 8
setvar 𝑦 |
10 | 9 | cv 1541 |
. . . . . . 7
class 𝑦 |
11 | | vz |
. . . . . . . 8
setvar 𝑧 |
12 | 11 | cv 1541 |
. . . . . . 7
class 𝑧 |
13 | | csdm 8888 |
. . . . . . 7
class
≺ |
14 | 10, 12, 13 | wbr 5109 |
. . . . . 6
wff 𝑦 ≺ 𝑧 |
15 | 14, 11, 3 | wrex 3070 |
. . . . 5
wff
∃𝑧 ∈
𝑥 𝑦 ≺ 𝑧 |
16 | 15, 9, 3 | wral 3061 |
. . . 4
wff
∀𝑦 ∈
𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 |
17 | 5, 8, 16 | w3a 1088 |
. . 3
wff (𝑥 ≠ ∅ ∧
(cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧) |
18 | 17, 2 | cab 2710 |
. 2
class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)} |
19 | 1, 18 | wceq 1542 |
1
wff
Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)} |