Theorem axc11n11r 36678

Description: Proof of axc11n 2425 from { ax-1 6-- ax-7 2008, axc9 2381, axc11r 2367 } (note that axc16 2262 is provable from { ax-1 6-- ax-7 2008, axc11r 2367 }).

Note that axc11n 2425 proves (over minimal calculus) that axc11 2429 and axc11r 2367 are equivalent. Therefore, axc11n11 36677 and axc11n11r 36678 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2429 appears slightly stronger since axc11n11r 36678 requires axc9 2381 while axc11n11 36677 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 2017	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		axc16 2262	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
3	1, 2	syl5 34	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
4	3	spsd 2188	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
5	4	exlimiv 1930	. 2 ⊢ (∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6		alnex 1781	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧∀𝑦 𝑦 = 𝑧)
7		ax6evr 2015	. . . . 5 ⊢ ∃𝑧 𝑥 = 𝑧
8		19.29 1873	. . . . 5 ⊢ ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
9	7, 8	mpan2 691	. . . 4 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧))
10		axc9 2381	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
11	10	impcom 407	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12		axc11r 2367	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
13	11, 12	syl9 77	. . . . . . . . . 10 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14		aev 2058	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
15	13, 14	syl8 76	. . . . . . . . 9 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
16	15	ex 412	. . . . . . . 8 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
17	16	com24 95	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
18	17	imp 406	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19		pm2.18 128	. . . . . 6 ⊢ ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
20	18, 19	syl6 35	. . . . 5 ⊢ ((¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
21	20	exlimiv 1930	. . . 4 ⊢ (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
22	9, 21	syl 17	. . 3 ⊢ (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
23	6, 22	sylbir 235	. 2 ⊢ (¬ ∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
24	5, 23	pm2.61i 182	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-12 2178  ax-13 2371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by: (None)