Theorem nla0002

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

	Ref	Expression
Hypotheses	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\}$$
	nla0001.set	$$⊢\phi \to A\in \mathrm{V}$$
	nla0002.sset	$$⊢\phi \to A\subseteq S$$
Assertion	nla0002	$$⊢\phi \to \varnothing \underset{\dot{}}{<}A$$

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		nla0001.set	$$⊢\phi \to A\in \mathrm{V}$$
3		nla0002.sset	$$⊢\phi \to A\subseteq S$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to \varnothing \in \mathrm{V}$$
6		0ss	$$⊢\varnothing \subseteq S$$
7	6	a1i	$$⊢\phi \to \varnothing \subseteq S$$
8		ral0	$$⊢\forall x\in \varnothing \forall y\in AxRy$$
9	8	a1i	$$⊢\phi \to \forall x\in \varnothing \forall y\in AxRy$$
10	7 3 9	3jca	$$⊢\phi \to \left(\varnothing \subseteq S\wedge A\subseteq S\wedge \forall x\in \varnothing \forall y\in AxRy\right)$$
11	1	rp-brsslt	$$⊢\varnothing \underset{\dot{}}{<}A\leftrightarrow \left(\left(\varnothing \in \mathrm{V}\wedge A\in \mathrm{V}\right)\wedge \left(\varnothing \subseteq S\wedge A\subseteq S\wedge \forall x\in \varnothing \forall y\in AxRy\right)\right)$$
12	5 2 10 11	syl21anbrc	$$⊢\phi \to \varnothing \underset{\dot{}}{<}A$$