Step |
Hyp |
Ref |
Expression |
1 |
|
axpowndlem4 |
⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) ) |
2 |
|
axpowndlem1 |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) |
3 |
2
|
aecoms |
⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) |
4 |
2
|
a1d |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) ) |
5 |
|
nfnae |
⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 |
6 |
|
nfae |
⊢ Ⅎ 𝑦 ∀ 𝑦 𝑦 = 𝑧 |
7 |
5 6
|
nfan |
⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) |
8 |
|
el |
⊢ ∃ 𝑤 𝑥 ∈ 𝑤 |
9 |
|
nfcvf2 |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ) |
10 |
|
nfcvd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 ) |
11 |
9 10
|
nfeld |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ∈ 𝑤 ) |
12 |
|
elequ2 |
⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) ) |
13 |
12
|
a1i |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) ) ) |
14 |
5 11 13
|
cbvexd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑤 𝑥 ∈ 𝑤 ↔ ∃ 𝑦 𝑥 ∈ 𝑦 ) ) |
15 |
8 14
|
mpbii |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 𝑥 ∈ 𝑦 ) |
16 |
15
|
19.8ad |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 𝑥 ∈ 𝑦 ) |
17 |
|
df-ex |
⊢ ( ∃ 𝑥 ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ¬ ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ) |
18 |
16 17
|
sylib |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ) |
19 |
18
|
adantr |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ¬ ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ) |
20 |
|
biidd |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑦 ) ) |
21 |
20
|
dral1 |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 ↔ ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 ) ) |
22 |
|
alnex |
⊢ ( ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ) |
23 |
|
alnex |
⊢ ( ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑧 𝑥 ∈ 𝑦 ) |
24 |
21 22 23
|
3bitr3g |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑧 𝑥 ∈ 𝑦 ) ) |
25 |
|
nd2 |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ¬ ∀ 𝑦 𝑥 ∈ 𝑧 ) |
26 |
|
mtt |
⊢ ( ¬ ∀ 𝑦 𝑥 ∈ 𝑧 → ( ¬ ∃ 𝑧 𝑥 ∈ 𝑦 ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) ) |
27 |
25 26
|
syl |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∃ 𝑧 𝑥 ∈ 𝑦 ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) ) |
28 |
24 27
|
bitrd |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) ) |
29 |
28
|
dral2 |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) ) |
30 |
29
|
adantl |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑥 ¬ ∃ 𝑦 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) ) |
31 |
19 30
|
mtbid |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ¬ ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) ) |
32 |
31
|
pm2.21d |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) |
33 |
7 32
|
alrimi |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) |
34 |
33
|
19.8ad |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) |
35 |
34
|
a1d |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) |
36 |
35
|
ex |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) ) |
37 |
4 36
|
pm2.61i |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) |
38 |
1 3 37
|
pm2.61ii |
⊢ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) |