Step | Hyp | Ref
| Expression |
1 | | en2lp 9351 |
. . . . . . . 8
⊢ ¬
(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) |
2 | | elequ2 2121 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧)) |
3 | 2 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
4 | 1, 3 | mtbii 326 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
5 | 4 | sps 2178 |
. . . . . 6
⊢
(∀𝑦 𝑦 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
6 | 5 | nexdv 1939 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → ¬ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
7 | 6 | pm2.21d 121 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
8 | 7 | axc4i 2316 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
9 | 8 | 19.8ad 2175 |
. 2
⊢
(∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
10 | | zfun 7579 |
. . 3
⊢
∃𝑥∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) |
11 | | nfnae 2434 |
. . . . 5
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑧 |
12 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
13 | | nfvd 1918 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 ∈ 𝑥) |
14 | | nfcvf 2936 |
. . . . . . . . 9
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑧) |
15 | 14 | nfcrd 2896 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑥 ∈ 𝑧) |
16 | 13, 15 | nfand 1900 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
17 | 12, 16 | nfexd 2323 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
18 | 17, 13 | nfimd 1897 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
19 | | elequ1 2113 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
20 | 19 | anbi1d 630 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
21 | 20 | exbidv 1924 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
22 | 21, 19 | imbi12d 345 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
23 | 22 | a1i 11 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑦 → ((∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
24 | 11, 18, 23 | cbvald 2407 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
25 | 24 | exbidv 1924 |
. . 3
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑥∀𝑤(∃𝑥(𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
26 | 10, 25 | mpbii 232 |
. 2
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
27 | 9, 26 | pm2.61i 182 |
1
⊢
∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) |