Mathbox for Wolf Lammen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-nax6al Structured version   Visualization version   GIF version

Theorem wl-nax6al 33842
 Description: In an empty domain the for-all operator always holds, even when applied to a false expression. This theorem actually shows that ax-5 2009 is provable there. Also we cannot assume that sp 2224 generally holds, except of course in the form of sptruw 1905. Without the support of an sp 2224 like theorem it seems difficult, if not impossible, to arrive at a theorem allowing to change the bounded variable in the antecedent. Additional axioms need to be postulated to further strengthen this result. A consequence of this result is that ∃𝑥𝜑 is not true for any 𝜑. In particular, ∃*𝑥𝜑 does not hold either, a somewhat counterintuitive result. (Contributed by Wolf Lammen, 12-Mar-2023.)
Assertion
Ref Expression
wl-nax6al (¬ ∃𝑥⊤ → ∀𝑥𝜑)

Proof of Theorem wl-nax6al
StepHypRef Expression
1 trud 1667 . . . 4 𝜑 → ⊤)
21eximi 1933 . . 3 (∃𝑥 ¬ 𝜑 → ∃𝑥⊤)
32con3i 152 . 2 (¬ ∃𝑥⊤ → ¬ ∃𝑥 ¬ 𝜑)
4 alex 1924 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
53, 4sylibr 226 1 (¬ ∃𝑥⊤ → ∀𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1654  ⊤wtru 1657  ∃wex 1878 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908 This theorem depends on definitions:  df-bi 199  df-tru 1660  df-ex 1879 This theorem is referenced by:  wl-nax6nfr  33843
 Copyright terms: Public domain W3C validator