Step | Hyp | Ref
| Expression |
1 | | 1on 6402 |
. . 3
⊢
1o ∈ On |
2 | 1 | elexi 2742 |
. 2
⊢
1o ∈ V |
3 | | elsni 3601 |
. . . . 5
⊢ (𝑦 ∈ {{𝑥 ∣ 𝜑}} → 𝑦 = {𝑥 ∣ 𝜑}) |
4 | | vprc 4121 |
. . . . . . . 8
⊢ ¬ V
∈ V |
5 | | df-v 2732 |
. . . . . . . . . 10
⊢ V =
{𝑥 ∣ 𝑥 = 𝑥} |
6 | | equid 1694 |
. . . . . . . . . . . 12
⊢ 𝑥 = 𝑥 |
7 | | pm5.1im 172 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑥 → (𝜑 → (𝑥 = 𝑥 ↔ 𝜑))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 = 𝑥 ↔ 𝜑)) |
9 | 8 | abbidv 2288 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑥 ∣ 𝑥 = 𝑥} = {𝑥 ∣ 𝜑}) |
10 | 5, 9 | eqtr2id 2216 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∣ 𝜑} = V) |
11 | 10 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝜑 → ({𝑥 ∣ 𝜑} ∈ V ↔ V ∈
V)) |
12 | 4, 11 | mtbiri 670 |
. . . . . . 7
⊢ (𝜑 → ¬ {𝑥 ∣ 𝜑} ∈ V) |
13 | | 19.8a 1583 |
. . . . . . . . 9
⊢ (𝑦 = {𝑥 ∣ 𝜑} → ∃𝑦 𝑦 = {𝑥 ∣ 𝜑}) |
14 | 3, 13 | syl 14 |
. . . . . . . 8
⊢ (𝑦 ∈ {{𝑥 ∣ 𝜑}} → ∃𝑦 𝑦 = {𝑥 ∣ 𝜑}) |
15 | | isset 2736 |
. . . . . . . 8
⊢ ({𝑥 ∣ 𝜑} ∈ V ↔ ∃𝑦 𝑦 = {𝑥 ∣ 𝜑}) |
16 | 14, 15 | sylibr 133 |
. . . . . . 7
⊢ (𝑦 ∈ {{𝑥 ∣ 𝜑}} → {𝑥 ∣ 𝜑} ∈ V) |
17 | 12, 16 | nsyl3 621 |
. . . . . 6
⊢ (𝑦 ∈ {{𝑥 ∣ 𝜑}} → ¬ 𝜑) |
18 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
19 | | biidd 171 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜑)) |
20 | 18, 19 | elab 2874 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
21 | 20 | notbii 663 |
. . . . . . . 8
⊢ (¬
𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ¬ 𝜑) |
22 | 21 | biimpri 132 |
. . . . . . 7
⊢ (¬
𝜑 → ¬ 𝑦 ∈ {𝑥 ∣ 𝜑}) |
23 | 22 | eq0rdv 3459 |
. . . . . 6
⊢ (¬
𝜑 → {𝑥 ∣ 𝜑} = ∅) |
24 | 17, 23 | syl 14 |
. . . . 5
⊢ (𝑦 ∈ {{𝑥 ∣ 𝜑}} → {𝑥 ∣ 𝜑} = ∅) |
25 | 3, 24 | eqtrd 2203 |
. . . 4
⊢ (𝑦 ∈ {{𝑥 ∣ 𝜑}} → 𝑦 = ∅) |
26 | | 0lt1o 6419 |
. . . 4
⊢ ∅
∈ 1o |
27 | 25, 26 | eqeltrdi 2261 |
. . 3
⊢ (𝑦 ∈ {{𝑥 ∣ 𝜑}} → 𝑦 ∈ 1o) |
28 | 27 | ssriv 3151 |
. 2
⊢ {{𝑥 ∣ 𝜑}} ⊆ 1o |
29 | 2, 28 | ssexi 4127 |
1
⊢ {{𝑥 ∣ 𝜑}} ∈ V |