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 36684
Description: Proof of axc11n 2431 from { ax-1 6-- ax-7 2007, axc9 2387, axc11r 2371 } (note that axc16 2261 is provable from { ax-1 6-- ax-7 2007, axc11r 2371 }).

Note that axc11n 2431 proves (over minimal calculus) that axc11 2435 and axc11r 2371 are equivalent. Therefore, axc11n11 36683 and axc11n11r 36684 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2435 appears slightly stronger since axc11n11r 36684 requires axc9 2387 while axc11n11 36683 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 2016 . . . . 5 (𝑥 = 𝑦𝑦 = 𝑥)
2 axc16 2261 . . . . 5 (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
31, 2syl5 34 . . . 4 (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
43spsd 2187 . . 3 (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
54exlimiv 1930 . 2 (∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6 alnex 1781 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧𝑦 𝑦 = 𝑧)
7 ax6evr 2014 . . . . 5 𝑧 𝑥 = 𝑧
8 19.29 1873 . . . . 5 ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
97, 8mpan2 691 . . . 4 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
10 axc9 2387 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
1110impcom 407 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12 axc11r 2371 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
1311, 12syl9 77 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14 aev 2057 . . . . . . . . . 10 (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
1513, 14syl8 76 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
1615ex 412 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
1716com24 95 . . . . . . 7 (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
1817imp 406 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19 pm2.18 128 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
2018, 19syl6 35 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
2120exlimiv 1930 . . . 4 (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
229, 21syl 17 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
236, 22sylbir 235 . 2 (¬ ∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
245, 23pm2.61i 182 1 (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-12 2177  ax-13 2377
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator