Theorem nulssgt

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

	Ref	Expression
Assertion	nulssgt	|- ( A e. ~P No -> A <

Proof

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