Theorem nulsslt

Description: The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	nulsslt	|- ( A e. ~P No -> (/) <

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. ~P No -> A e. _V )
2		0ex	|- (/) e. _V
3	1 2	jctil	|- ( A e. ~P No -> ( (/) e. _V /\ A e. _V ) )
4		0ss	|- (/) C_ No
5	4	a1i	|- ( A e. ~P No -> (/) C_ No )
6		elpwi	|- ( A e. ~P No -> A C_ No )
7		ral0	|- A. x e. (/) A. y e. A x
8	7	a1i	|- ( A e. ~P No -> A. x e. (/) A. y e. A x
9	5 6 8	3jca	|- ( A e. ~P No -> ( (/) C_ No /\ A C_ No /\ A. x e. (/) A. y e. A x
10		brsslt	|- ( (/) < ( ( (/) e. _V /\ A e. _V ) /\ ( (/) C_ No /\ A C_ No /\ A. x e. (/) A. y e. A x
11	3 9 10	sylanbrc	|- ( A e. ~P No -> (/) <