Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axc11n11r Structured version   Visualization version   GIF version

Theorem axc11n11r 35556
Description: Proof of axc11n 2425 from { ax-1 6-- ax-7 2011, axc9 2381, axc11r 2365 } (note that axc16 2252 is provable from { ax-1 6-- ax-7 2011, axc11r 2365 }).

Note that axc11n 2425 proves (over minimal calculus) that axc11 2429 and axc11r 2365 are equivalent. Therefore, axc11n11 35555 and axc11n11r 35556 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 35556 requires axc9 2381 while axc11n11 35555 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.
StepHypRef Expression
1 equcomi 2020 . . . . 5 (𝑥 = 𝑦𝑦 = 𝑥)
2 axc16 2252 . . . . 5 (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
31, 2syl5 34 . . . 4 (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
43spsd 2180 . . 3 (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
54exlimiv 1933 . 2 (∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6 alnex 1783 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧𝑦 𝑦 = 𝑧)
7 ax6evr 2018 . . . . 5 𝑧 𝑥 = 𝑧
8 19.29 1876 . . . . 5 ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
97, 8mpan2 689 . . . 4 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
10 axc9 2381 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
1110impcom 408 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12 axc11r 2365 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
1311, 12syl9 77 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14 aev 2060 . . . . . . . . . 10 (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
1513, 14syl8 76 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
1615ex 413 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
1716com24 95 . . . . . . 7 (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
1817imp 407 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19 pm2.18 128 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
2018, 19syl6 35 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
2120exlimiv 1933 . . . 4 (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
229, 21syl 17 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
236, 22sylbir 234 . 2 (¬ ∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
245, 23pm2.61i 182 1 (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wal 1539  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-12 2171  ax-13 2371
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator