Theorem axc11n11r 37416

Description: Proof of axc11n 2455 from { ax-1 6-- ax-7 2041, axc9 2411, axc11r 2397 } (note that axc16 2295 is provable from { ax-1 6-- ax-7 2041, axc11r 2397 }).

Note that axc11n 2455 proves (over minimal calculus) that axc11 2459 and axc11r 2397 are equivalent. Therefore, axc11n11 37415 and axc11n11r 37416 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2459 appears slightly stronger since axc11n11r 37416 requires axc9 2411 while axc11n11 37415 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 2050	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		axc16 2295	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
3	1, 2	syl5 35	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
4	3	spsd 2223	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
5	4	exlimiv 1963	. 2 ⊢ (∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6		alnex 1814	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧∀𝑦 𝑦 = 𝑧)
7		ax6evr 2048	. . . . 5 ⊢ ∃𝑧 𝑥 = 𝑧
8		19.29 1906	. . . . 5 ⊢ ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
9	7, 8	mpan2 704	. . . 4 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
10		axc9 2411	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
11	10	impcom 413	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12		axc11r 2397	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
13	11, 12	syl9 78	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14		aev 2092	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
15	13, 14	syl8 77	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
16	15	ex 418	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
17	16	com24 96	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
18	17	imp 412	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19		pm2.18 129	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
20	18, 19	syl6 36	. . . . 5 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
21	20	exlimiv 1963	. . . 4 ⊢ (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
22	9, 21	syl 18	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
23	6, 22	sylbir 238	. 2 ⊢ (¬ ∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
24	5, 23	pm2.61i 184	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-12 2213  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by: (None)