Theorem sssslt2

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

	Ref	Expression
Assertion	sssslt2	|- ( ( A < A <

Proof

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