Step | Hyp | Ref
| Expression |
1 | | eleq12 2235 |
. . . . . . 7
⊢ ((𝑦 = {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∧ 𝑦 = {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥}) → (𝑦 ∈ 𝑦 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥})) |
2 | 1 | anidms 395 |
. . . . . 6
⊢ (𝑦 = {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} → (𝑦 ∈ 𝑦 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥})) |
3 | 2 | notbid 662 |
. . . . 5
⊢ (𝑦 = {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} → (¬ 𝑦 ∈ 𝑦 ↔ ¬ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥})) |
4 | | df-nel 2436 |
. . . . . . 7
⊢ (𝑥 ∉ 𝑥 ↔ ¬ 𝑥 ∈ 𝑥) |
5 | | eleq12 2235 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
6 | 5 | anidms 395 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
7 | 6 | notbid 662 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦)) |
8 | 4, 7 | syl5bb 191 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∉ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦)) |
9 | 8 | cbvrabv 2729 |
. . . . 5
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦} |
10 | 3, 9 | elrab2 2889 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ↔ ({𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝐴 ∧ ¬ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥})) |
11 | | pclem6 1369 |
. . . 4
⊢ (({𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ↔ ({𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝐴 ∧ ¬ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥})) → ¬ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝐴) |
12 | 10, 11 | ax-mp 5 |
. . 3
⊢ ¬
{𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝐴 |
13 | | ssel 3141 |
. . 3
⊢
(𝒫 𝐴 ⊆
𝐴 → ({𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝒫 𝐴 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝐴)) |
14 | 12, 13 | mtoi 659 |
. 2
⊢
(𝒫 𝐴 ⊆
𝐴 → ¬ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝒫 𝐴) |
15 | | ssrab2 3232 |
. . 3
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ⊆ 𝐴 |
16 | | elpw2g 4140 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ({𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝒫 𝐴 ↔ {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ⊆ 𝐴)) |
17 | 15, 16 | mpbiri 167 |
. 2
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∉ 𝑥} ∈ 𝒫 𝐴) |
18 | 14, 17 | nsyl3 621 |
1
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴) |