Theorem axc11n11r 31860

Description: Proof of axc11n 2295 from { ax-1 6-- ax-7 1922, axc9 2290, axc11r 2175 } (note that axc16 2120 is provable from { ax-1 6-- ax-7 1922, axc11r 2175 }).

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

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

Assertion

Ref	Expression
axc11n11r	⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Proof of Theorem axc11n11r

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equcomi 1931	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		axc16 2120	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
3	1, 2	syl5 33	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
4	3	spsd 2045	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
5	4	exlimiv 1845	. 2 ⊢ (∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6		alnex 1697	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧∀𝑦 𝑦 = 𝑧)
7		ax6evr 1929	. . . . 5 ⊢ ∃𝑧 𝑥 = 𝑧
8		19.29 1789	. . . . 5 ⊢ ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
9	7, 8	mpan2 703	. . . 4 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
10		axc9 2290	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
11	10	impcom 445	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12		axc11r 2175	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
13	11, 12	syl9 75	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14		aev 1970	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
15	13, 14	syl8 74	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
16	15	ex 449	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
17	16	com24 93	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
18	17	imp 444	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19		pm2.18 121	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
20	18, 19	syl6 34	. . . . 5 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
21	20	exlimiv 1845	. . . 4 ⊢ (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
22	9, 21	syl 17	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
23	6, 22	sylbir 224	. 2 ⊢ (¬ ∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
24	5, 23	pm2.61i 175	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by: (None)