Step | Hyp | Ref
| Expression |
1 | | axinfndlem1 10219 |
. . . . . . 7
⊢
(∀𝑥 𝑤 ∈ 𝑧 → ∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
2 | 1 | ax-gen 1803 |
. . . . . 6
⊢
∀𝑤(∀𝑥 𝑤 ∈ 𝑧 → ∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
3 | | nfnae 2433 |
. . . . . . . 8
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑥 |
4 | | nfnae 2433 |
. . . . . . . 8
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑧 |
5 | 3, 4 | nfan 1907 |
. . . . . . 7
⊢
Ⅎ𝑦(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
6 | | nfnae 2433 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑥 |
7 | | nfnae 2433 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
8 | 6, 7 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑥(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
9 | | nfcvd 2905 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦𝑤) |
10 | | nfcvf 2933 |
. . . . . . . . . . 11
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑧) |
11 | 10 | adantl 485 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦𝑧) |
12 | 9, 11 | nfeld 2915 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑤 ∈ 𝑧) |
13 | 8, 12 | nfald 2327 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑥 𝑤 ∈ 𝑧) |
14 | | nfcvf 2933 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥) |
15 | 14 | adantr 484 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦𝑥) |
16 | 9, 15 | nfeld 2915 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑤 ∈ 𝑥) |
17 | | nfnae 2433 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑤 ¬
∀𝑦 𝑦 = 𝑥 |
18 | | nfnae 2433 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑤 ¬
∀𝑦 𝑦 = 𝑧 |
19 | 17, 18 | nfan 1907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
20 | | nfnae 2433 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧 ¬
∀𝑦 𝑦 = 𝑥 |
21 | | nfnae 2433 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧 ¬
∀𝑦 𝑦 = 𝑧 |
22 | 20, 21 | nfan 1907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
23 | 11, 15 | nfeld 2915 |
. . . . . . . . . . . . . 14
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑧 ∈ 𝑥) |
24 | 12, 23 | nfand 1905 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) |
25 | 22, 24 | nfexd 2328 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) |
26 | 16, 25 | nfimd 1902 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) |
27 | 19, 26 | nfald 2327 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) |
28 | 16, 27 | nfand 1905 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
29 | 8, 28 | nfexd 2328 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
30 | 13, 29 | nfimd 1902 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦(∀𝑥 𝑤 ∈ 𝑧 → ∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
31 | | nfcvd 2905 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑥𝑤) |
32 | | nfcvf2 2934 |
. . . . . . . . . . . . 13
⊢ (¬
∀𝑦 𝑦 = 𝑥 → Ⅎ𝑥𝑦) |
33 | 32 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑥𝑦) |
34 | 31, 33 | nfeqd 2914 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑥 𝑤 = 𝑦) |
35 | 8, 34 | nfan1 2198 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) |
36 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → 𝑤 = 𝑦) |
37 | 36 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑤 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) |
38 | 35, 37 | albid 2220 |
. . . . . . . . 9
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∀𝑥 𝑤 ∈ 𝑧 ↔ ∀𝑥 𝑦 ∈ 𝑧)) |
39 | 36 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
40 | | nfcvd 2905 |
. . . . . . . . . . . . . . . . . 18
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧𝑤) |
41 | | nfcvf2 2934 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦) |
42 | 41 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧𝑦) |
43 | 40, 42 | nfeqd 2914 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑦) |
44 | 22, 43 | nfan1 2198 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) |
45 | 37 | anbi1d 633 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ((𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) |
46 | 44, 45 | exbid 2221 |
. . . . . . . . . . . . . . 15
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) |
47 | 39, 46 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ((𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
48 | 47 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → ((𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
49 | 5, 26, 48 | cbvald 2406 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
50 | 49 | adantr 484 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
51 | 39, 50 | anbi12d 634 |
. . . . . . . . . 10
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ((𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
52 | 35, 51 | exbid 2221 |
. . . . . . . . 9
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
53 | 38, 52 | imbi12d 348 |
. . . . . . . 8
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ((∀𝑥 𝑤 ∈ 𝑧 → ∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) ↔ (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))) |
54 | 53 | ex 416 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → ((∀𝑥 𝑤 ∈ 𝑧 → ∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) ↔ (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))))) |
55 | 5, 30, 54 | cbvald 2406 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑤(∀𝑥 𝑤 ∈ 𝑧 → ∃𝑥(𝑤 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑥 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) ↔ ∀𝑦(∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))) |
56 | 2, 55 | mpbii 236 |
. . . . 5
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑦(∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
57 | 56 | 19.21bi 2186 |
. . . 4
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
58 | 57 | ex 416 |
. . 3
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))) |
59 | | nd1 10201 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑦 ∈ 𝑧) |
60 | 59 | aecoms 2427 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑥 → ¬ ∀𝑥 𝑦 ∈ 𝑧) |
61 | 60 | pm2.21d 121 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
62 | | nd3 10203 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → ¬ ∀𝑥 𝑦 ∈ 𝑧) |
63 | 62 | pm2.21d 121 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
64 | 58, 61, 63 | pm2.61ii 186 |
. 2
⊢
(∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
65 | 64 | 19.35ri 1887 |
1
⊢
∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |