Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-nax6im | Structured version Visualization version GIF version |
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 2061 requires us to formally assign a boolean value to an equation, say always false, unless you want to give up on exmid 923, for example. Whatever it is, we start out with the contraposition of ax-6 2075, 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 could be. (Contributed by Wolf Lammen, 12-Mar-2023.) |
Ref | Expression |
---|---|
wl-nax6im.1 | ⊢ (¬ ∃𝑥 𝑥 = 𝑦 → 𝜑) |
Ref | Expression |
---|---|
wl-nax6im | ⊢ (¬ ∃𝑥⊤ → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trud 1667 | . . . 4 ⊢ (𝑥 = 𝑦 → ⊤) | |
2 | 1 | eximi 1933 | . . 3 ⊢ (∃𝑥 𝑥 = 𝑦 → ∃𝑥⊤) |
3 | wl-nax6im.1 | . . 3 ⊢ (¬ ∃𝑥 𝑥 = 𝑦 → 𝜑) | |
4 | 2, 3 | nsyl4 158 | . 2 ⊢ (¬ 𝜑 → ∃𝑥⊤) |
5 | 4 | con1i 147 | 1 ⊢ (¬ ∃𝑥⊤ → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ⊤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: (None) |
Copyright terms: Public domain | W3C validator |