Metamath Proof Explorer

Theorem axinfprim

Description: ax-inf without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010)

Ref Expression
Assertion axinfprim ⊢ ¬ ∀ x ¬ y ∈ z → ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x

Proof

Step Hyp Ref Expression
1 axinfnd ⊢ ∃ x y ∈ z → y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x
2 df-an ⊢ y ∈ z ∧ z ∈ x ↔ ¬ y ∈ z → ¬ z ∈ x
3 2 exbii ⊢ ∃ z y ∈ z ∧ z ∈ x ↔ ∃ z ¬ y ∈ z → ¬ z ∈ x
4 exnal ⊢ ∃ z ¬ y ∈ z → ¬ z ∈ x ↔ ¬ ∀ z y ∈ z → ¬ z ∈ x
5 3 4 bitri ⊢ ∃ z y ∈ z ∧ z ∈ x ↔ ¬ ∀ z y ∈ z → ¬ z ∈ x
6 5 imbi2i ⊢ y ∈ x → ∃ z y ∈ z ∧ z ∈ x ↔ y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
7 6 albii ⊢ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x ↔ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
8 7 anbi2i ⊢ y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x ↔ y ∈ x ∧ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
9 df-an ⊢ y ∈ x ∧ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x ↔ ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
10 8 9 bitri ⊢ y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x ↔ ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
11 10 imbi2i ⊢ y ∈ z → y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x ↔ y ∈ z → ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
12 11 exbii ⊢ ∃ x y ∈ z → y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x ↔ ∃ x y ∈ z → ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
13 df-ex ⊢ ∃ x y ∈ z → ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x ↔ ¬ ∀ x ¬ y ∈ z → ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
14 12 13 bitri ⊢ ∃ x y ∈ z → y ∈ x ∧ ∀ y y ∈ x → ∃ z y ∈ z ∧ z ∈ x ↔ ¬ ∀ x ¬ y ∈ z → ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x
15 1 14 mpbi ⊢ ¬ ∀ x ¬ y ∈ z → ¬ y ∈ x → ¬ ∀ y y ∈ x → ¬ ∀ z y ∈ z → ¬ z ∈ x