Metamath Proof Explorer

Theorem axc11n11r

Description: Proof of axc11n from { ax-1 -- ax-7 , axc9 , axc11r } (note that axc16 is provable from { ax-1 -- ax-7 , axc11r }).

Note that axc11n proves (over minimal calculus) that axc11 and axc11r are equivalent. Therefore, axc11n11 and axc11n11r prove that one can use one or the other as an axiom, provided one assumes the axioms listed above ( axc11 appears slightly stronger since axc11n11r requires axc9 while axc11n11 does not).

(Contributed by BJ, 6-Jul-2021) (Proof modification is discouraged.)

Ref Expression
Assertion axc11n11r ⊢ ∀ x x = y → ∀ y y = x

Proof

Step Hyp Ref Expression
1 equcomi ⊢ x = y → y = x
2 axc16 ⊢ ∀ y y = z → y = x → ∀ y y = x
3 1 2 syl5 ⊢ ∀ y y = z → x = y → ∀ y y = x
4 3 spsd ⊢ ∀ y y = z → ∀ x x = y → ∀ y y = x
5 4 exlimiv ⊢ ∃ z ∀ y y = z → ∀ x x = y → ∀ y y = x
6 alnex ⊢ ∀ z ¬ ∀ y y = z ↔ ¬ ∃ z ∀ y y = z
7 ax6evr ⊢ ∃ z x = z
8 19.29 ⊢ ∀ z ¬ ∀ y y = z ∧ ∃ z x = z → ∃ z ¬ ∀ y y = z ∧ x = z
9 7 8 mpan2 ⊢ ∀ z ¬ ∀ y y = z → ∃ z ¬ ∀ y y = z ∧ x = z
10 axc9 ⊢ ¬ ∀ y y = x → ¬ ∀ y y = z → x = z → ∀ y x = z
11 10 impcom ⊢ ¬ ∀ y y = z ∧ ¬ ∀ y y = x → x = z → ∀ y x = z
12 axc11r ⊢ ∀ x x = y → ∀ y x = z → ∀ x x = z
13 11 12 syl9 ⊢ ¬ ∀ y y = z ∧ ¬ ∀ y y = x → ∀ x x = y → x = z → ∀ x x = z
14 aev ⊢ ∀ x x = z → ∀ y y = x
15 13 14 syl8 ⊢ ¬ ∀ y y = z ∧ ¬ ∀ y y = x → ∀ x x = y → x = z → ∀ y y = x
16 15 ex ⊢ ¬ ∀ y y = z → ¬ ∀ y y = x → ∀ x x = y → x = z → ∀ y y = x
17 16 com24 ⊢ ¬ ∀ y y = z → x = z → ∀ x x = y → ¬ ∀ y y = x → ∀ y y = x
18 17 imp ⊢ ¬ ∀ y y = z ∧ x = z → ∀ x x = y → ¬ ∀ y y = x → ∀ y y = x
19 pm2.18 ⊢ ¬ ∀ y y = x → ∀ y y = x → ∀ y y = x
20 18 19 syl6 ⊢ ¬ ∀ y y = z ∧ x = z → ∀ x x = y → ∀ y y = x
21 20 exlimiv ⊢ ∃ z ¬ ∀ y y = z ∧ x = z → ∀ x x = y → ∀ y y = x
22 9 21 syl ⊢ ∀ z ¬ ∀ y y = z → ∀ x x = y → ∀ y y = x
23 6 22 sylbir ⊢ ¬ ∃ z ∀ y y = z → ∀ x x = y → ∀ y y = x
24 5 23 pm2.61i ⊢ ∀ x x = y → ∀ y y = x