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

Theorem axc11n11r 31860
 Description: Proof of axc11n 2295 from { ax-1 6-- ax-7 1922, axc9 2290, axc11r 2175 } (note that axc16 2120 is provable from { ax-1 6-- ax-7 1922, axc11r 2175 }). Note that axc11n 2295 proves (over minimal calculus) that axc11 2302 and axc11r 2175 are equivalent. Therefore, axc11n11 31859 and axc11n11r 31860 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2302 appears slightly stronger since axc11n11r 31860 requires axc9 2290 while axc11n11 31859 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 1931 . . . . 5 (𝑥 = 𝑦𝑦 = 𝑥)
2 axc16 2120 . . . . 5 (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
31, 2syl5 33 . . . 4 (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
43spsd 2045 . . 3 (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
54exlimiv 1845 . 2 (∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6 alnex 1697 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧𝑦 𝑦 = 𝑧)
7 ax6evr 1929 . . . . 5 𝑧 𝑥 = 𝑧
8 19.29 1789 . . . . 5 ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
97, 8mpan2 703 . . . 4 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
10 axc9 2290 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
1110impcom 445 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12 axc11r 2175 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
1311, 12syl9 75 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14 aev 1970 . . . . . . . . . 10 (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
1513, 14syl8 74 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
1615ex 449 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
1716com24 93 . . . . . . 7 (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
1817imp 444 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19 pm2.18 121 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
2018, 19syl6 34 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
2120exlimiv 1845 . . . 4 (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
229, 21syl 17 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
236, 22sylbir 224 . 2 (¬ ∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
245, 23pm2.61i 175 1 (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator