Metamath Proof Explorer

Theorem axacprim

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

Ref Expression
Assertion axacprim ⊢ ¬ ∀ x ¬ ∀ y ∀ z ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x

Proof

Step Hyp Ref Expression
1 axacnd ⊢ ∃ x ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
2 df-an ⊢ y ∈ z ∧ z ∈ w ↔ ¬ y ∈ z → ¬ z ∈ w
3 2 albii ⊢ ∀ x y ∈ z ∧ z ∈ w ↔ ∀ x ¬ y ∈ z → ¬ z ∈ w
4 anass ⊢ y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x
5 annim ⊢ z ∈ w ∧ ¬ y ∈ w → ¬ w ∈ x ↔ ¬ z ∈ w → y ∈ w → ¬ w ∈ x
6 pm4.63 ⊢ ¬ y ∈ w → ¬ w ∈ x ↔ y ∈ w ∧ w ∈ x
7 6 anbi2i ⊢ z ∈ w ∧ ¬ y ∈ w → ¬ w ∈ x ↔ z ∈ w ∧ y ∈ w ∧ w ∈ x
8 5 7 bitr3i ⊢ ¬ z ∈ w → y ∈ w → ¬ w ∈ x ↔ z ∈ w ∧ y ∈ w ∧ w ∈ x
9 8 anbi2i ⊢ y ∈ z ∧ ¬ z ∈ w → y ∈ w → ¬ w ∈ x ↔ y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x
10 annim ⊢ y ∈ z ∧ ¬ z ∈ w → y ∈ w → ¬ w ∈ x ↔ ¬ y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
11 4 9 10 3bitr2i ⊢ y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ ¬ y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
12 11 exbii ⊢ ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ ∃ w ¬ y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
13 exnal ⊢ ∃ w ¬ y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x ↔ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
14 12 13 bitri ⊢ ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
15 14 bibi1i ⊢ ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x ↔ y = w
16 dfbi1 ⊢ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x ↔ y = w ↔ ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
17 15 16 bitri ⊢ ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
18 17 albii ⊢ ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
19 18 exbii ⊢ ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ∃ w ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
20 df-ex ⊢ ∃ w ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x ↔ ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
21 19 20 bitri ⊢ ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
22 3 21 imbi12i ⊢ ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
23 22 2albii ⊢ ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ∀ y ∀ z ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
24 23 exbii ⊢ ∃ x ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ∃ x ∀ y ∀ z ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
25 df-ex ⊢ ∃ x ∀ y ∀ z ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x ↔ ¬ ∀ x ¬ ∀ y ∀ z ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
26 24 25 bitri ⊢ ∃ x ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w ↔ ¬ ∀ x ¬ ∀ y ∀ z ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x
27 1 26 mpbi ⊢ ¬ ∀ x ¬ ∀ y ∀ z ∀ x ¬ y ∈ z → ¬ z ∈ w → ¬ ∀ w ¬ ∀ y ¬ ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x → y = w → ¬ y = w → ¬ ∀ w y ∈ z → z ∈ w → y ∈ w → ¬ w ∈ x