Theorem ssltun2

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

	Ref	Expression
Assertion	ssltun2	|- ( ( 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		ssltex2	|- ( A < C e. _V )
5		unexg	|- ( ( B e. _V /\ C e. _V ) -> ( B u. C ) e. _V )
6	3 4 5	syl2an	|- ( ( A < ( B u. C ) e. _V )
7	2 6	jca	|- ( ( A < ( A e. _V /\ ( B u. C ) e. _V ) )
8		ssltss1	|- ( A < A C_ No )
9	8	adantr	|- ( ( A < A C_ No )
10		ssltss2	|- ( A < B C_ No )
11	10	adantr	|- ( ( A < B C_ No )
12		ssltss2	|- ( A < C C_ No )
13	12	adantl	|- ( ( A < C C_ No )
14	11 13	unssd	|- ( ( A < ( B u. C ) C_ No )
15		ssltsep	|- ( A < A. x e. A A. y e. B x
16	15	adantr	|- ( ( A < A. x e. A A. y e. B x
17		ssltsep	|- ( A < A. x e. A A. y e. C x
18	17	adantl	|- ( ( A < A. x e. A A. y e. C x
19		ralunb	|- ( A. y e. ( B u. C ) x ( A. y e. B x
20	19	ralbii	|- ( A. x e. A A. y e. ( B u. C ) x A. x e. A ( A. y e. B x
21		r19.26	|- ( A. x e. A ( A. y e. B x ( A. x e. A A. y e. B x
22	20 21	bitri	|- ( A. x e. A A. y e. ( B u. C ) x ( A. x e. A A. y e. B x
23	16 18 22	sylanbrc	|- ( ( A < A. x e. A A. y e. ( B u. C ) x
24	9 14 23	3jca	|- ( ( A < ( A C_ No /\ ( B u. C ) C_ No /\ A. x e. A A. y e. ( B u. C ) x
25		brsslt	|- ( A < ( ( A e. _V /\ ( B u. C ) e. _V ) /\ ( A C_ No /\ ( B u. C ) C_ No /\ A. x e. A A. y e. ( B u. C ) x
26	7 24 25	sylanbrc	|- ( ( A < A <