This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid ⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
14 13 ex ⊢ ( ¬ 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) )
15 ax13b ⊢ ( ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) ↔ ( ¬ 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) ) )
16 14 15 mpbir ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )