Theorem nla0003

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

	Ref	Expression
Hypotheses	nla0001.defsslt	$$⊢\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	nla0003	$$⊢\phi \to A\underset{\dot{}}{<}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nla0001.defsslt	$$⊢\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 y\in \varnothing \forall x\in AxRy$$
9		ralcom	$$⊢\forall y\in \varnothing \forall x\in AxRy\leftrightarrow \forall x\in A\forall y\in \varnothing xRy$$
10	8 9	mpbi	$$⊢\forall x\in A\forall y\in \varnothing xRy$$
11	10	a1i	$$⊢\phi \to \forall x\in A\forall y\in \varnothing xRy$$
12	3 7 11	3jca	$$⊢\phi \to \left(A\subseteq S\wedge \varnothing \subseteq S\wedge \forall x\in A\forall y\in \varnothing xRy\right)$$
13	1	rp-brsslt	$$⊢A\underset{\dot{}}{<}\varnothing \leftrightarrow \left(\left(A\in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\wedge \left(A\subseteq S\wedge \varnothing \subseteq S\wedge \forall x\in A\forall y\in \varnothing xRy\right)\right)$$
14	2 5 12 13	syl21anbrc	$$⊢\phi \to A\underset{\dot{}}{<}\varnothing$$