Theorem ax13

Description: Derive ax-13 from ax13v and Tarski's FOL. This shows that the weakening in ax13v is still sufficient for a complete system. Preferably, use the weaker ax13w to avoid the propagation of ax-13 . (Contributed by NM, 21-Dec-2015) (Proof shortened by Wolf Lammen, 31-Jan-2018) Reduce axiom usage. (Revised by Wolf Lammen, 2-Jun-2021) (New usage is discouraged.)

	Ref	Expression
Assertion	ax13	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		equvinv	⊢ ( 𝑦 = 𝑧 ↔ ∃ 𝑤 ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) )
2		ax13lem1	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ∀ 𝑥 𝑤 = 𝑦 ) )
3	2	imp	⊢ ( ( ¬ 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ∀ 𝑥 𝑤 = 𝑦 )
4		ax13lem1	⊢ ( ¬ 𝑥 = 𝑧 → ( 𝑤 = 𝑧 → ∀ 𝑥 𝑤 = 𝑧 ) )
5	4	imp	⊢ ( ( ¬ 𝑥 = 𝑧 ∧ 𝑤 = 𝑧 ) → ∀ 𝑥 𝑤 = 𝑧 )
6		ax7v1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 = 𝑧 → 𝑦 = 𝑧 ) )
7	6	imp	⊢ ( ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) → 𝑦 = 𝑧 )
8	7	alanimi	⊢ ( ( ∀ 𝑥 𝑤 = 𝑦 ∧ ∀ 𝑥 𝑤 = 𝑧 ) → ∀ 𝑥 𝑦 = 𝑧 )
9	3 5 8	syl2an	⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) ∧ ( ¬ 𝑥 = 𝑧 ∧ 𝑤 = 𝑧 ) ) → ∀ 𝑥 𝑦 = 𝑧 )
10	9	an4s	⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) ∧ ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) ) → ∀ 𝑥 𝑦 = 𝑧 )
11	10	ex	⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) → ( ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) → ∀ 𝑥 𝑦 = 𝑧 ) )
12	11	exlimdv	⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) → ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) → ∀ 𝑥 𝑦 = 𝑧 ) )
13	1 12	syl5bi	⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
14	13	ex	⊢ ( ¬ 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) )
15		ax13b	⊢ ( ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) ↔ ( ¬ 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) ) )
16	14 15	mpbir	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )