Step |
Hyp |
Ref |
Expression |
1 |
|
sn-el |
⊢ ∃ 𝑤 ∃ 𝑥 𝑥 ∈ 𝑤 |
2 |
|
ax-nul |
⊢ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 |
3 |
|
exdistrv |
⊢ ( ∃ 𝑤 ∃ 𝑧 ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ↔ ( ∃ 𝑤 ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ) |
4 |
1 2 3
|
mpbir2an |
⊢ ∃ 𝑤 ∃ 𝑧 ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) |
5 |
|
ax9v1 |
⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧 ) ) |
6 |
5
|
eximdv |
⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑥 𝑥 ∈ 𝑤 → ∃ 𝑥 𝑥 ∈ 𝑧 ) ) |
7 |
|
df-ex |
⊢ ( ∃ 𝑥 𝑥 ∈ 𝑧 ↔ ¬ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) |
8 |
6 7
|
syl6ib |
⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑥 𝑥 ∈ 𝑤 → ¬ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ) |
9 |
|
imnan |
⊢ ( ( ∃ 𝑥 𝑥 ∈ 𝑤 → ¬ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ↔ ¬ ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ) |
10 |
8 9
|
sylib |
⊢ ( 𝑤 = 𝑧 → ¬ ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) ) |
11 |
10
|
con2i |
⊢ ( ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) → ¬ 𝑤 = 𝑧 ) |
12 |
11
|
2eximi |
⊢ ( ∃ 𝑤 ∃ 𝑧 ( ∃ 𝑥 𝑥 ∈ 𝑤 ∧ ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 ) → ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 ) |
13 |
|
equeuclr |
⊢ ( 𝑧 = 𝑦 → ( 𝑤 = 𝑦 → 𝑤 = 𝑧 ) ) |
14 |
13
|
con3d |
⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ¬ 𝑤 = 𝑦 ) ) |
15 |
|
ax7v1 |
⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → 𝑤 = 𝑦 ) ) |
16 |
15
|
con3d |
⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦 ) ) |
17 |
16
|
spimevw |
⊢ ( ¬ 𝑤 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
18 |
14 17
|
syl6 |
⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) ) |
19 |
|
ax7v1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) ) |
20 |
19
|
con3d |
⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦 ) ) |
21 |
20
|
spimevw |
⊢ ( ¬ 𝑧 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
22 |
21
|
a1d |
⊢ ( ¬ 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) ) |
23 |
18 22
|
pm2.61i |
⊢ ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
24 |
23
|
exlimivv |
⊢ ( ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
25 |
4 12 24
|
mp2b |
⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦 |
26 |
|
exnal |
⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) |
27 |
25 26
|
mpbi |
⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 |