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 33001
Description: Proof of axc11n 2451 from { ax-1 6-- ax-7 2090, axc9 2447, axc11r 2332 } (note that axc16 2282 is provable from { ax-1 6-- ax-7 2090, axc11r 2332 }).

Note that axc11n 2451 proves (over minimal calculus) that axc11 2456 and axc11r 2332 are equivalent. Therefore, axc11n11 33000 and axc11n11r 33001 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2456 appears slightly stronger since axc11n11r 33001 requires axc9 2447 while axc11n11 33000 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 2099 . . . . 5 (𝑥 = 𝑦𝑦 = 𝑥)
2 axc16 2282 . . . . 5 (∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
31, 2syl5 34 . . . 4 (∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
43spsd 2204 . . 3 (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
54exlimiv 2007 . 2 (∃𝑧𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
6 alnex 1855 . . 3 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧𝑦 𝑦 = 𝑧)
7 ax6evr 2097 . . . . 5 𝑧 𝑥 = 𝑧
8 19.29 1950 . . . . 5 ((∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
97, 8mpan2 709 . . . 4 (∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧))
10 axc9 2447 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)))
1110impcom 445 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
12 axc11r 2332 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
1311, 12syl9 77 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)))
14 aev 2134 . . . . . . . . . 10 (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
1513, 14syl8 76 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))
1615ex 449 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))))
1716com24 95 . . . . . . 7 (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))))
1817imp 444 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
19 pm2.18 122 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥)
2018, 19syl6 35 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥))
2120exlimiv 2007 . . . 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 1630  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-12 2196  ax-13 2391
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator