Theorem wl-nax6im 34752

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 1960 requires us to formally assign a boolean value to an equation, say always false, unless you want to give up on exmid 891, for example. Whatever it is, we start out with the contraposition of ax-6 1966, 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

Step	Hyp	Ref	Expression
1		trud 1543	. . . 4 ⊢ (𝑥 = 𝑦 → ⊤)
2	1	eximi 1831	. . 3 ⊢ (∃𝑥 𝑥 = 𝑦 → ∃𝑥⊤)
3		wl-nax6im.1	. . 3 ⊢ (¬ ∃𝑥 𝑥 = 𝑦 → 𝜑)
4	2, 3	nsyl4 161	. 2 ⊢ (¬ 𝜑 → ∃𝑥⊤)
5	4	con1i 149	1 ⊢ (¬ ∃𝑥⊤ → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ⊤wtru 1534  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806

This theorem depends on definitions:  df-bi 209  df-tru 1536  df-ex 1777

This theorem is referenced by: (None)