Proof of Theorem axinfprim
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | axinfnd 10647 | . 2
⊢
∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) | 
| 2 |  | df-an 396 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥) ↔ ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)) | 
| 3 | 2 | exbii 1847 | . . . . . . . . . 10
⊢
(∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)) | 
| 4 |  | exnal 1826 | . . . . . . . . . 10
⊢
(∃𝑧 ¬
(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥) ↔ ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)) | 
| 5 | 3, 4 | bitri 275 | . . . . . . . . 9
⊢
(∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥) ↔ ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)) | 
| 6 | 5 | imbi2i 336 | . . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) ↔ (𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))) | 
| 7 | 6 | albii 1818 | . . . . . . 7
⊢
(∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)) ↔ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))) | 
| 8 | 7 | anbi2i 623 | . . . . . 6
⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) | 
| 9 |  | df-an 396 | . . . . . 6
⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))) ↔ ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) | 
| 10 | 8, 9 | bitri 275 | . . . . 5
⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ↔ ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) | 
| 11 | 10 | imbi2i 336 | . . . 4
⊢ ((𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) ↔ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))) | 
| 12 | 11 | exbii 1847 | . . 3
⊢
(∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) ↔ ∃𝑥(𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))) | 
| 13 |  | df-ex 1779 | . . 3
⊢
(∃𝑥(𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) ↔ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))) | 
| 14 | 12, 13 | bitri 275 | . 2
⊢
(∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) ↔ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))) | 
| 15 | 1, 14 | mpbi 230 | 1
⊢  ¬
∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥)))) |