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

Theorem wl-nax6im 38232
Description: The following series of theorems are centered around the empty domain, where no set exists. As a consequence, a set variable like 𝑥 has no instance to assign to. An expression like 𝑥 = 𝑦 is not really meaningful then. What does it evaluate to, true or false? In fact, the grammar extension weq 1995 requires us to formally assign a boolean value to an equation, say always false, unless you want to give up on exmid 908, for example. Whatever it is, we start out with the contraposition of ax-6 2000, that guarantees the existence of at least one set. Our hypothesis here expresses tentatively it might not hold. We can simplify the antecedent then, to the point where we do not need equation any more. This suggests what a decent characterization of the empty domain of discourse could be. (Contributed by Wolf Lammen, 12-Mar-2023.)
Hypothesis
Ref Expression
wl-nax6im.1 (¬ ∃𝑥 𝑥 = 𝑦𝜑)
Assertion
Ref Expression
wl-nax6im (¬ ∃𝑥⊤ → 𝜑)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥, 𝑦)

Proof of Theorem wl-nax6im
StepHypRef Expression
1 trud 1580 . . 3 (𝑥 = 𝑦 → ⊤)
21eximi 1868 . 2 (∃𝑥 𝑥 = 𝑦 → ∃𝑥⊤)
3 wl-nax6im.1 . 2 (¬ ∃𝑥 𝑥 = 𝑦𝜑)
42, 3nsyl5 160 1 (¬ ∃𝑥⊤ → 𝜑)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3  wi 4  wtru 1571  wex 1812
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842
This proof depends on definitions:  df-bi 210  df-tru 1573  df-ex 1813
This theorem is used by: (None)
  Copyright terms: Public domain W3C validator