Theorem sssslt2

Description: Relationship 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	12	adantr	|- ( ( A < A. x e. A A. y e. B x
14		ssralv	|- ( C C_ B -> ( A. y e. B x A. y e. C x
15	5 14	syl	|- ( ( A < ( A. y e. B x A. y e. C x
16	15	ralimdv	|- ( ( A < ( A. x e. A A. y e. B x A. x e. A A. y e. C x
17	13 16	mpd	|- ( ( A < A. x e. A A. y e. C x
18	8 11 17	3jca	|- ( ( A < ( A C_ No /\ C C_ No /\ A. x e. A A. y e. C x
19		brsslt	|- ( A < ( ( A e. _V /\ C e. _V ) /\ ( A C_ No /\ C C_ No /\ A. x e. A A. y e. C x
20	2 6 18 19	syl21anbrc	|- ( ( A < A <