Step |
Hyp |
Ref |
Expression |
0 |
|
cnp |
⊢ P |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
c0 |
⊢ ∅ |
3 |
1
|
cv |
⊢ 𝑥 |
4 |
2 3
|
wpss |
⊢ ∅ ⊊ 𝑥 |
5 |
|
cnq |
⊢ Q |
6 |
3 5
|
wpss |
⊢ 𝑥 ⊊ Q |
7 |
4 6
|
wa |
⊢ ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) |
8 |
|
vy |
⊢ 𝑦 |
9 |
|
vz |
⊢ 𝑧 |
10 |
9
|
cv |
⊢ 𝑧 |
11 |
|
cltq |
⊢ <Q |
12 |
8
|
cv |
⊢ 𝑦 |
13 |
10 12 11
|
wbr |
⊢ 𝑧 <Q 𝑦 |
14 |
10 3
|
wcel |
⊢ 𝑧 ∈ 𝑥 |
15 |
13 14
|
wi |
⊢ ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) |
16 |
15 9
|
wal |
⊢ ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) |
17 |
12 10 11
|
wbr |
⊢ 𝑦 <Q 𝑧 |
18 |
17 9 3
|
wrex |
⊢ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 |
19 |
16 18
|
wa |
⊢ ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) |
20 |
19 8 3
|
wral |
⊢ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) |
21 |
7 20
|
wa |
⊢ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) |
22 |
21 1
|
cab |
⊢ { 𝑥 ∣ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) } |
23 |
0 22
|
wceq |
⊢ P = { 𝑥 ∣ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) } |