Step | Hyp | Ref
| Expression |
1 | | en2lp 8510 |
. . . . . . . 8
⊢ ¬
(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) |
2 | | elequ2 2004 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧)) |
3 | 2 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
4 | 1, 3 | mtbii 316 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
5 | 4 | sps 2055 |
. . . . . 6
⊢
(∀𝑦 𝑦 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
6 | 5 | nexdv 1864 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → ¬ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
7 | 6 | pm2.21d 118 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
8 | 7 | axc4i 2131 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
9 | | 19.8a 2052 |
. . 3
⊢
(∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
10 | 8, 9 | syl 17 |
. 2
⊢
(∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
11 | | zfun 6950 |
. . 3
⊢
∃𝑥∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) |
12 | | nfnae 2318 |
. . . . 5
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑧 |
13 | | nfnae 2318 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
14 | | nfvd 1844 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 ∈ 𝑥) |
15 | | nfcvf 2788 |
. . . . . . . . 9
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑧) |
16 | 15 | nfcrd 2771 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥 ∈ 𝑧) |
17 | 14, 16 | nfand 1826 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
18 | 13, 17 | nfexd 2167 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
19 | 18, 14 | nfimd 1823 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
20 | | elequ1 1997 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
21 | 20 | anbi1d 741 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
22 | 21 | exbidv 1850 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
23 | 22, 20 | imbi12d 334 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
24 | 23 | a1i 11 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑦 → ((∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
25 | 12, 19, 24 | cbvald 2277 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
26 | 25 | exbidv 1850 |
. . 3
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑥∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
27 | 11, 26 | mpbii 223 |
. 2
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
28 | 10, 27 | pm2.61i 176 |
1
⊢
∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) |