Theorem nla0001

Description: Extending a linear order to subsets, the empty set is less than itself. Note in Alling, p. 3. (Contributed by RP, 28-Nov-2023)

	Ref	Expression
Hypothesis	nla0001.defslts	$$⊢\underset{\dot{}}{<}=\left\{⟨a,b⟩|\left(a\subseteq S\wedge b\subseteq S\wedge \forall x\in a\forall y\in bxRy\right)\right\}$$
Assertion	nla0001	$$⊢\phi \to \varnothing \underset{\dot{}}{<}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nla0001.defslts	$$⊢\underset{\dot{}}{<}=\left\{⟨a,b⟩|\left(a\subseteq S\wedge b\subseteq S\wedge \forall x\in a\forall y\in bxRy\right)\right\}$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	a1i	$$⊢\phi \to \varnothing \in \mathrm{V}$$
4		0ss	$$⊢\varnothing \subseteq S$$
5	4	a1i	$$⊢\phi \to \varnothing \subseteq S$$
6	1 3 5	nla0002	$$⊢\phi \to \varnothing \underset{\dot{}}{<}\varnothing$$