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