Theorem axc11n11r 37026

Description: Proof of axc11n 2434 from { ax-1 6-- ax-7 2015, axc9 2390, axc11r 2376 } (note that axc16 2273 is provable from { ax-1 6-- ax-7 2015, axc11r 2376 }).

Note that axc11n 2434 proves (over minimal calculus) that axc11 2438 and axc11r 2376 are equivalent. Therefore, axc11n11 37025 and axc11n11r 37026 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2438 appears slightly stronger since axc11n11r 37026 requires axc9 2390 while axc11n11 37025 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 2024	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		axc16 2273	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
3	1, 2	syl5 34	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
4	3	spsd 2199	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
5	4	exlimiv 1937	. 2 ⊢ (∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6		alnex 1788	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧∀𝑦 𝑦 = 𝑧)
7		ax6evr 2022	. . . . 5 ⊢ ∃𝑧 𝑥 = 𝑧
8		19.29 1880	. . . . 5 ⊢ ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
9	7, 8	mpan2 697	. . . 4 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
10		axc9 2390	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
11	10	impcom 408	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12		axc11r 2376	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
13	11, 12	syl9 77	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14		aev 2066	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
15	13, 14	syl8 76	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
16	15	ex 413	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
17	16	com24 95	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
18	17	imp 407	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19		pm2.18 128	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
20	18, 19	syl6 35	. . . . 5 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
21	20	exlimiv 1937	. . . 4 ⊢ (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
22	9, 21	syl 17	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
23	6, 22	sylbir 236	. 2 ⊢ (¬ ∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
24	5, 23	pm2.61i 183	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-12 2189  ax-13 2380

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791

This theorem is referenced by: (None)