Detailed syntax breakdown of Definition df-np
Step | Hyp | Ref
| Expression |
1 | | cnp 10616 |
. 2
class
P |
2 | | c0 4262 |
. . . . . 6
class
∅ |
3 | | vx |
. . . . . . 7
setvar 𝑥 |
4 | 3 | cv 1541 |
. . . . . 6
class 𝑥 |
5 | 2, 4 | wpss 3893 |
. . . . 5
wff ∅
⊊ 𝑥 |
6 | | cnq 10609 |
. . . . . 6
class
Q |
7 | 4, 6 | wpss 3893 |
. . . . 5
wff 𝑥 ⊊
Q |
8 | 5, 7 | wa 396 |
. . . 4
wff (∅
⊊ 𝑥 ∧ 𝑥 ⊊
Q) |
9 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
10 | 9 | cv 1541 |
. . . . . . . . 9
class 𝑧 |
11 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
12 | 11 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
13 | | cltq 10615 |
. . . . . . . . 9
class
<Q |
14 | 10, 12, 13 | wbr 5079 |
. . . . . . . 8
wff 𝑧 <Q
𝑦 |
15 | 9, 3 | wel 2111 |
. . . . . . . 8
wff 𝑧 ∈ 𝑥 |
16 | 14, 15 | wi 4 |
. . . . . . 7
wff (𝑧 <Q
𝑦 → 𝑧 ∈ 𝑥) |
17 | 16, 9 | wal 1540 |
. . . . . 6
wff
∀𝑧(𝑧 <Q
𝑦 → 𝑧 ∈ 𝑥) |
18 | 12, 10, 13 | wbr 5079 |
. . . . . . 7
wff 𝑦 <Q
𝑧 |
19 | 18, 9, 4 | wrex 3067 |
. . . . . 6
wff
∃𝑧 ∈
𝑥 𝑦 <Q 𝑧 |
20 | 17, 19 | wa 396 |
. . . . 5
wff
(∀𝑧(𝑧 <Q
𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧) |
21 | 20, 11, 4 | wral 3066 |
. . . 4
wff
∀𝑦 ∈
𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧) |
22 | 8, 21 | wa 396 |
. . 3
wff ((∅
⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧
∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧)) |
23 | 22, 3 | cab 2717 |
. 2
class {𝑥 ∣ ((∅ ⊊
𝑥 ∧ 𝑥 ⊊ Q) ∧
∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))} |
24 | 1, 23 | wceq 1542 |
1
wff
P = {𝑥
∣ ((∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧
∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))} |