Theorem ssltun1

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

	Ref	Expression
Assertion	ssltun1	|- ( ( A < ( A u. B ) <

Proof

Step	Hyp	Ref	Expression
1		ssltex1	|- ( A < A e. _V )
2		ssltex1	|- ( B < B e. _V )
3		unexg	|- ( ( A e. _V /\ B e. _V ) -> ( A u. B ) e. _V )
4	1 2 3	syl2an	|- ( ( A < ( A u. B ) e. _V )
5		ssltex2	|- ( A < C e. _V )
6	5	adantr	|- ( ( A < C e. _V )
7	4 6	jca	|- ( ( A < ( ( A u. B ) e. _V /\ C e. _V ) )
8		ssltss1	|- ( A < A C_ No )
9	8	adantr	|- ( ( A < A C_ No )
10		ssltss1	|- ( B < B C_ No )
11	10	adantl	|- ( ( A < B C_ No )
12	9 11	unssd	|- ( ( A < ( A u. B ) C_ No )
13		ssltss2	|- ( B < C C_ No )
14	13	adantl	|- ( ( A < C C_ No )
15		ssltsep	|- ( A < A. x e. A A. y e. C x
16	15	adantr	|- ( ( A < A. x e. A A. y e. C x
17		ssltsep	|- ( B < A. x e. B A. y e. C x
18	17	adantl	|- ( ( A < A. x e. B A. y e. C x
19		ralunb	|- ( A. x e. ( A u. B ) A. y e. C x ( A. x e. A A. y e. C x
20	16 18 19	sylanbrc	|- ( ( A < A. x e. ( A u. B ) A. y e. C x
21	12 14 20	3jca	|- ( ( A < ( ( A u. B ) C_ No /\ C C_ No /\ A. x e. ( A u. B ) A. y e. C x
22		brsslt	|- ( ( A u. B ) < ( ( ( A u. B ) e. _V /\ C e. _V ) /\ ( ( A u. B ) C_ No /\ C C_ No /\ A. x e. ( A u. B ) A. y e. C x
23	7 21 22	sylanbrc	|- ( ( A < ( A u. B ) <