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	|- .< = { <. 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	nla0003	|- ( 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. y e. (/) A. x e. A x R y
9		ralcom	|- ( A. y e. (/) A. x e. A x R y <-> A. x e. A A. y e. (/) x R y )
10	8 9	mpbi	|- A. x e. A A. y e. (/) x R y
11	10	a1i	|- ( ph -> A. x e. A A. y e. (/) x R y )
12	3 7 11	3jca	|- ( ph -> ( A C_ S /\ (/) C_ S /\ A. x e. A A. y e. (/) x R y ) )
13	1	rp-brsslt	|- ( A .< (/) <-> ( ( A e. _V /\ (/) e. _V ) /\ ( A C_ S /\ (/) C_ S /\ A. x e. A A. y e. (/) x R y ) ) )
14	2 5 12 13	syl21anbrc	|- ( ph -> A .< (/) )