Theorem axc11n11r 37196

Description: Proof of axc11n 2464 from { ax-1 6-- ax-7 2035, axc9 2420, axc11r 2406 } (note that axc16 2303 is provable from { ax-1 6-- ax-7 2035, axc11r 2406 }).

Note that axc11n 2464 proves (over minimal calculus) that axc11 2468 and axc11r 2406 are equivalent. Therefore, axc11n11 37195 and axc11n11r 37196 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2468 appears slightly stronger since axc11n11r 37196 requires axc9 2420 while axc11n11 37195 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 2044	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		axc16 2303	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
3	1, 2	syl5 35	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
4	3	spsd 2229	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
5	4	exlimiv 1957	. 2 ⊢ (∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6		alnex 1808	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧∀𝑦 𝑦 = 𝑧)
7		ax6evr 2042	. . . . 5 ⊢ ∃𝑧 𝑥 = 𝑧
8		19.29 1900	. . . . 5 ⊢ ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
9	7, 8	mpan2 703	. . . 4 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
10		axc9 2420	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
11	10	impcom 412	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12		axc11r 2406	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
13	11, 12	syl9 78	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14		aev 2086	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
15	13, 14	syl8 77	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
16	15	ex 417	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
17	16	com24 96	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
18	17	imp 411	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19		pm2.18 129	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
20	18, 19	syl6 36	. . . . 5 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
21	20	exlimiv 1957	. . . 4 ⊢ (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
22	9, 21	syl 18	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
23	6, 22	sylbir 238	. 2 ⊢ (¬ ∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
24	5, 23	pm2.61i 184	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400  ∀wal 1565  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-12 2219  ax-13 2410

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811

This theorem is referenced by: (None)