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 32950
Description: Proof of axc11n 2439 from { ax-1 6-- ax-7 2078, axc9 2435, axc11r 2320 } (note that axc16 2270 is provable from { ax-1 6-- ax-7 2078, axc11r 2320 }).

Note that axc11n 2439 proves (over minimal calculus) that axc11 2444 and axc11r 2320 are equivalent. Therefore, axc11n11 32949 and axc11n11r 32950 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2444 appears slightly stronger since axc11n11r 32950 requires axc9 2435 while axc11n11 32949 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 2087 . . . . 5 (𝑥 = 𝑦𝑦 = 𝑥)
2 axc16 2270 . . . . 5 (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
31, 2syl5 34 . . . 4 (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
43spsd 2192 . . 3 (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
54exlimiv 1995 . 2 (∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6 alnex 1843 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧𝑦 𝑦 = 𝑧)
7 ax6evr 2085 . . . . 5 𝑧 𝑥 = 𝑧
8 19.29 1938 . . . . 5 ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
97, 8mpan2 709 . . . 4 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
10 axc9 2435 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
1110impcom 445 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12 axc11r 2320 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
1311, 12syl9 77 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14 aev 2122 . . . . . . . . . 10 (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
1513, 14syl8 76 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
1615ex 449 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
1716com24 95 . . . . . . 7 (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
1817imp 444 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19 pm2.18 122 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
2018, 19syl6 35 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
2120exlimiv 1995 . . . 4 (∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
229, 21syl 17 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
236, 22sylbir 225 . 2 (¬ ∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
245, 23pm2.61i 176 1 (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wal 1618  wex 1841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-10 2156  ax-12 2184  ax-13 2379
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator