Step | Hyp | Ref
| Expression |
1 | | vprc 3888 |
. . . 4
⊢ ¬ V
∈ V |
2 | | vex 2560 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
3 | 2 | snid 3402 |
. . . . . . . . 9
⊢ 𝑧 ∈ {𝑧} |
4 | | a9ev 1587 |
. . . . . . . . . 10
⊢
∃𝑦 𝑦 = 𝑧 |
5 | | sneq 3386 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → {𝑧} = {𝑦}) |
6 | 5 | equcoms 1594 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → {𝑧} = {𝑦}) |
7 | 4, 6 | eximii 1493 |
. . . . . . . . 9
⊢
∃𝑦{𝑧} = {𝑦} |
8 | | snexgOLD 3935 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → {𝑧} ∈ V) |
9 | 2, 8 | ax-mp 7 |
. . . . . . . . . 10
⊢ {𝑧} ∈ V |
10 | | eleq2 2101 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑧} → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ {𝑧})) |
11 | | eqeq1 2046 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑧} → (𝑥 = {𝑦} ↔ {𝑧} = {𝑦})) |
12 | 11 | exbidv 1706 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑧} → (∃𝑦 𝑥 = {𝑦} ↔ ∃𝑦{𝑧} = {𝑦})) |
13 | 10, 12 | anbi12d 442 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑧} → ((𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦}) ↔ (𝑧 ∈ {𝑧} ∧ ∃𝑦{𝑧} = {𝑦}))) |
14 | 9, 13 | spcev 2647 |
. . . . . . . . 9
⊢ ((𝑧 ∈ {𝑧} ∧ ∃𝑦{𝑧} = {𝑦}) → ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦})) |
15 | 3, 7, 14 | mp2an 402 |
. . . . . . . 8
⊢
∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦}) |
16 | | eluniab 3592 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ↔ ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦})) |
17 | 15, 16 | mpbir 134 |
. . . . . . 7
⊢ 𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} |
18 | 17, 2 | 2th 163 |
. . . . . 6
⊢ (𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ↔ 𝑧 ∈ V) |
19 | 18 | eqriv 2037 |
. . . . 5
⊢ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} = V |
20 | 19 | eleq1i 2103 |
. . . 4
⊢ (∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ∈ V ↔ V ∈
V) |
21 | 1, 20 | mtbir 596 |
. . 3
⊢ ¬
∪ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V |
22 | | uniexg 4175 |
. . 3
⊢ ({𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V → ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ∈ V) |
23 | 21, 22 | mto 588 |
. 2
⊢ ¬
{𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V |
24 | 23 | nelir 2300 |
1
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V |