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 ¬ ∀ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ¬ ( 𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤 ) → ¬ ∀ 𝑤 ¬ ∀ 𝑦 ¬ ( ( ¬ ∀ 𝑤 ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ 𝑤 → ( 𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥 ) ) ) → 𝑦 = 𝑤 ) → ¬ ( 𝑦 = 𝑤 → ¬ ∀ 𝑤 ( 𝑦 ∈ 𝑧 → ( 𝑧 ∈ 𝑤 → ( 𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥 ) ) ) ) ) )

Proof

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