Step | Hyp | Ref
| Expression |
1 | | 0ex 4116 |
. . . . . . . . 9
⊢ ∅
∈ V |
2 | 1 | snid 3614 |
. . . . . . . 8
⊢ ∅
∈ {∅} |
3 | | nnexmid 845 |
. . . . . . . . . . 11
⊢ ¬
¬ (𝑦 = {∅} ∨
¬ 𝑦 =
{∅}) |
4 | | uneq1 3274 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = {∅} → (𝑦 ∪ ({∅} ∖ 𝑦)) = ({∅} ∪ ({∅}
∖ 𝑦))) |
5 | | undifabs 3491 |
. . . . . . . . . . . . . . 15
⊢
({∅} ∪ ({∅} ∖ 𝑦)) = {∅} |
6 | 4, 5 | eqtrdi 2219 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = {∅} → (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅}) |
7 | 6 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ {∅} → (𝑦 = {∅} → (𝑦 ∪ ({∅} ∖ 𝑦)) =
{∅})) |
8 | | df-ne 2341 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ≠ {∅} ↔ ¬
𝑦 =
{∅}) |
9 | | pwntru 4185 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ {∅} ∧ 𝑦 ≠ {∅}) → 𝑦 = ∅) |
10 | 8, 9 | sylan2br 286 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ {∅} ∧ ¬
𝑦 = {∅}) → 𝑦 = ∅) |
11 | 10 | difeq2d 3245 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ {∅} ∧ ¬
𝑦 = {∅}) →
({∅} ∖ 𝑦) =
({∅} ∖ ∅)) |
12 | | dif0 3485 |
. . . . . . . . . . . . . . . . 17
⊢
({∅} ∖ ∅) = {∅} |
13 | 11, 12 | eqtrdi 2219 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ {∅} ∧ ¬
𝑦 = {∅}) →
({∅} ∖ 𝑦) =
{∅}) |
14 | 10, 13 | uneq12d 3282 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ {∅} ∧ ¬
𝑦 = {∅}) →
(𝑦 ∪ ({∅} ∖
𝑦)) = (∅ ∪
{∅})) |
15 | | uncom 3271 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∪ {∅}) = ({∅} ∪ ∅) |
16 | | un0 3448 |
. . . . . . . . . . . . . . . 16
⊢
({∅} ∪ ∅) = {∅} |
17 | 15, 16 | eqtri 2191 |
. . . . . . . . . . . . . . 15
⊢ (∅
∪ {∅}) = {∅} |
18 | 14, 17 | eqtrdi 2219 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ {∅} ∧ ¬
𝑦 = {∅}) →
(𝑦 ∪ ({∅} ∖
𝑦)) =
{∅}) |
19 | 18 | ex 114 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ {∅} → (¬
𝑦 = {∅} → (𝑦 ∪ ({∅} ∖ 𝑦)) =
{∅})) |
20 | 7, 19 | jaod 712 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ {∅} →
((𝑦 = {∅} ∨ ¬
𝑦 = {∅}) →
(𝑦 ∪ ({∅} ∖
𝑦)) =
{∅})) |
21 | 20 | con3d 626 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ {∅} → (¬
(𝑦 ∪ ({∅} ∖
𝑦)) = {∅} →
¬ (𝑦 = {∅} ∨
¬ 𝑦 =
{∅}))) |
22 | 3, 21 | mtoi 659 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ {∅} → ¬
¬ (𝑦 ∪ ({∅}
∖ 𝑦)) =
{∅}) |
23 | 22 | adantl 275 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → ¬ ¬ (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅}) |
24 | | difss 3253 |
. . . . . . . . . . . . 13
⊢
({∅} ∖ 𝑦) ⊆ {∅} |
25 | | unss 3301 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ {∅} ∧
({∅} ∖ 𝑦)
⊆ {∅}) ↔ (𝑦 ∪ ({∅} ∖ 𝑦)) ⊆ {∅}) |
26 | 25 | biimpi 119 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ {∅} ∧
({∅} ∖ 𝑦)
⊆ {∅}) → (𝑦 ∪ ({∅} ∖ 𝑦)) ⊆ {∅}) |
27 | 24, 26 | mpan2 423 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ {∅} → (𝑦 ∪ ({∅} ∖ 𝑦)) ⊆
{∅}) |
28 | 27 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → (𝑦 ∪ ({∅} ∖ 𝑦)) ⊆
{∅}) |
29 | | exmid1stab.x |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) →
STAB 𝑥 =
{∅}) |
30 | 29 | ex 114 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ⊆ {∅} → STAB
𝑥 =
{∅})) |
31 | 30 | alrimiv 1867 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥(𝑥 ⊆ {∅} → STAB
𝑥 =
{∅})) |
32 | | p0ex 4174 |
. . . . . . . . . . . . . 14
⊢ {∅}
∈ V |
33 | 32 | ssex 4126 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∪ ({∅} ∖ 𝑦)) ⊆ {∅} →
(𝑦 ∪ ({∅} ∖
𝑦)) ∈
V) |
34 | | sseq1 3170 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 ∪ ({∅} ∖ 𝑦)) → (𝑥 ⊆ {∅} ↔ (𝑦 ∪ ({∅} ∖ 𝑦)) ⊆ {∅})) |
35 | | eqeq1 2177 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 ∪ ({∅} ∖ 𝑦)) → (𝑥 = {∅} ↔ (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅})) |
36 | 35 | stbid 827 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 ∪ ({∅} ∖ 𝑦)) → (STAB 𝑥 = {∅} ↔
STAB (𝑦
∪ ({∅} ∖ 𝑦)) = {∅})) |
37 | 34, 36 | imbi12d 233 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ ({∅} ∖ 𝑦)) → ((𝑥 ⊆ {∅} → STAB
𝑥 = {∅}) ↔
((𝑦 ∪ ({∅}
∖ 𝑦)) ⊆
{∅} → STAB (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅}))) |
38 | 37 | spcgv 2817 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∪ ({∅} ∖ 𝑦)) ∈ V →
(∀𝑥(𝑥 ⊆ {∅} →
STAB 𝑥 =
{∅}) → ((𝑦 ∪
({∅} ∖ 𝑦))
⊆ {∅} → STAB (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅}))) |
39 | 27, 33, 38 | 3syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ {∅} →
(∀𝑥(𝑥 ⊆ {∅} →
STAB 𝑥 =
{∅}) → ((𝑦 ∪
({∅} ∖ 𝑦))
⊆ {∅} → STAB (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅}))) |
40 | 31, 39 | mpan9 279 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → ((𝑦 ∪ ({∅} ∖ 𝑦)) ⊆ {∅} →
STAB (𝑦
∪ ({∅} ∖ 𝑦)) = {∅})) |
41 | 28, 40 | mpd 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) →
STAB (𝑦
∪ ({∅} ∖ 𝑦)) = {∅}) |
42 | | df-stab 826 |
. . . . . . . . . 10
⊢
(STAB (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅} ↔ (¬ ¬ (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅} → (𝑦 ∪ ({∅} ∖ 𝑦)) =
{∅})) |
43 | 41, 42 | sylib 121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → (¬ ¬
(𝑦 ∪ ({∅} ∖
𝑦)) = {∅} →
(𝑦 ∪ ({∅} ∖
𝑦)) =
{∅})) |
44 | 23, 43 | mpd 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → (𝑦 ∪ ({∅} ∖ 𝑦)) = {∅}) |
45 | 2, 44 | eleqtrrid 2260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → ∅ ∈
(𝑦 ∪ ({∅} ∖
𝑦))) |
46 | | elun 3268 |
. . . . . . 7
⊢ (∅
∈ (𝑦 ∪ ({∅}
∖ 𝑦)) ↔ (∅
∈ 𝑦 ∨ ∅
∈ ({∅} ∖ 𝑦))) |
47 | 45, 46 | sylib 121 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → (∅ ∈
𝑦 ∨ ∅ ∈
({∅} ∖ 𝑦))) |
48 | | eldifn 3250 |
. . . . . . 7
⊢ (∅
∈ ({∅} ∖ 𝑦) → ¬ ∅ ∈ 𝑦) |
49 | 48 | orim2i 756 |
. . . . . 6
⊢ ((∅
∈ 𝑦 ∨ ∅
∈ ({∅} ∖ 𝑦)) → (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦)) |
50 | 47, 49 | syl 14 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → (∅ ∈
𝑦 ∨ ¬ ∅ ∈
𝑦)) |
51 | | df-dc 830 |
. . . . 5
⊢
(DECID ∅ ∈ 𝑦 ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦)) |
52 | 50, 51 | sylibr 133 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) →
DECID ∅ ∈ 𝑦) |
53 | 52 | ex 114 |
. . 3
⊢ (𝜑 → (𝑦 ⊆ {∅} →
DECID ∅ ∈ 𝑦)) |
54 | 53 | alrimiv 1867 |
. 2
⊢ (𝜑 → ∀𝑦(𝑦 ⊆ {∅} →
DECID ∅ ∈ 𝑦)) |
55 | | df-exmid 4181 |
. 2
⊢
(EXMID ↔ ∀𝑦(𝑦 ⊆ {∅} →
DECID ∅ ∈ 𝑦)) |
56 | 54, 55 | sylibr 133 |
1
⊢ (𝜑 →
EXMID) |