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.defsslt	|- .< = { <. a , b >. | ( a C_ S /\ b C_ S /\ A. x e. a A. y e. b x R y ) }
	nla0001.set	|- ( ph -> A e. _V )
	nla0002.sset	|- ( ph -> A C_ S )
Assertion	nla0002	|- ( ph -> (/) .< A )

Proof

Step	Hyp	Ref	Expression
1		nla0001.defsslt	|- .< = { <. a , b >. | ( a C_ S /\ b C_ S /\ A. x e. a A. y e. b x R y ) }
2		nla0001.set	|- ( ph -> A e. _V )
3		nla0002.sset	|- ( ph -> A C_ S )
4		0ex	|- (/) e. _V
5	4	a1i	|- ( ph -> (/) e. _V )
6		0ss	|- (/) C_ S
7	6	a1i	|- ( ph -> (/) C_ S )
8		ral0	|- A. x e. (/) A. y e. A x R y
9	8	a1i	|- ( ph -> A. x e. (/) A. y e. A x R y )
10	7 3 9	3jca	|- ( ph -> ( (/) C_ S /\ A C_ S /\ A. x e. (/) A. y e. A x R y ) )
11	1	rp-brsslt	|- ( (/) .< A <-> ( ( (/) e. _V /\ A e. _V ) /\ ( (/) C_ S /\ A C_ S /\ A. x e. (/) A. y e. A x R y ) ) )
12	5 2 10 11	syl21anbrc	|- ( ph -> (/) .< A )