Theorem sssslt1

Description: Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021)

	Ref	Expression
Assertion	sssslt1	|- ( ( A < C <

Proof

Step	Hyp	Ref	Expression
1		ssltex1	|- ( A < A e. _V )
2	1	adantr	|- ( ( A < A e. _V )
3		simpr	|- ( ( A < C C_ A )
4	2 3	ssexd	|- ( ( A < C e. _V )
5		ssltex2	|- ( A < B e. _V )
6	5	adantr	|- ( ( A < B e. _V )
7		ssltss1	|- ( A < A C_ No )
8	7	adantr	|- ( ( A < A C_ No )
9	3 8	sstrd	|- ( ( A < C C_ No )
10		ssltss2	|- ( A < B C_ No )
11	10	adantr	|- ( ( A < B C_ No )
12		ssltsep	|- ( A < A. x e. A A. y e. B x
13		ssralv	|- ( C C_ A -> ( A. x e. A A. y e. B x A. x e. C A. y e. B x
14	12 13	mpan9	|- ( ( A < A. x e. C A. y e. B x
15	9 11 14	3jca	|- ( ( A < ( C C_ No /\ B C_ No /\ A. x e. C A. y e. B x
16		brsslt	|- ( C < ( ( C e. _V /\ B e. _V ) /\ ( C C_ No /\ B C_ No /\ A. x e. C A. y e. B x
17	4 6 15 16	syl21anbrc	|- ( ( A < C <