Theorem sslttr

Description: Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( B =/= (/) <-> E. y y e. B )
2		ssltex1	|- ( A < A e. _V )
3	2	3ad2ant2	|- ( ( y e. B /\ A < A e. _V )
4		ssltex2	|- ( B < C e. _V )
5	4	3ad2ant3	|- ( ( y e. B /\ A < C e. _V )
6		ssltss1	|- ( A < A C_ No )
7	6	3ad2ant2	|- ( ( y e. B /\ A < A C_ No )
8		ssltss2	|- ( B < C C_ No )
9	8	3ad2ant3	|- ( ( y e. B /\ A < C C_ No )
10	7	3ad2ant1	|- ( ( ( y e. B /\ A < A C_ No )
11		simp2	|- ( ( ( y e. B /\ A < x e. A )
12	10 11	sseldd	|- ( ( ( y e. B /\ A < x e. No )
13		ssltss2	|- ( A < B C_ No )
14	13	3ad2ant2	|- ( ( y e. B /\ A < B C_ No )
15	14	3ad2ant1	|- ( ( ( y e. B /\ A < B C_ No )
16		simp11	|- ( ( ( y e. B /\ A < y e. B )
17	15 16	sseldd	|- ( ( ( y e. B /\ A < y e. No )
18	9	3ad2ant1	|- ( ( ( y e. B /\ A < C C_ No )
19		simp3	|- ( ( ( y e. B /\ A < z e. C )
20	18 19	sseldd	|- ( ( ( y e. B /\ A < z e. No )
21		simp12	|- ( ( ( y e. B /\ A < A <
22	21 11 16	ssltsepcd	|- ( ( ( y e. B /\ A < x
23		simp13	|- ( ( ( y e. B /\ A < B <
24	23 16 19	ssltsepcd	|- ( ( ( y e. B /\ A < y
25	12 17 20 22 24	slttrd	|- ( ( ( y e. B /\ A < x
26	3 5 7 9 25	ssltd	|- ( ( y e. B /\ A < A <
27	26	3exp	|- ( y e. B -> ( A < ( B < A <
28	27	exlimiv	|- ( E. y y e. B -> ( A < ( B < A <
29	1 28	sylbi	|- ( B =/= (/) -> ( A < ( B < A <
30	29	3imp231	|- ( ( A < A <