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	1	adantr	|- ( ( A < A e. _V )
3		ssltex1	|- ( B < B e. _V )
4	3	adantl	|- ( ( A < B e. _V )
5	2 4	unexd	|- ( ( A < ( A u. B ) e. _V )
6		ssltex2	|- ( A < C e. _V )
7	6	adantr	|- ( ( A < 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	|- ( A < C C_ No )
14	13	adantr	|- ( ( A < C C_ No )
15		elun	|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
16		ssltsepc	|- ( ( A < x
17	16	3exp	|- ( A < ( x e. A -> ( y e. C -> x
18	17	adantr	|- ( ( A < ( x e. A -> ( y e. C -> x
19	18	com12	|- ( x e. A -> ( ( A < ( y e. C -> x
20		ssltsepc	|- ( ( B < x
21	20	3exp	|- ( B < ( x e. B -> ( y e. C -> x
22	21	adantl	|- ( ( A < ( x e. B -> ( y e. C -> x
23	22	com12	|- ( x e. B -> ( ( A < ( y e. C -> x
24	19 23	jaoi	|- ( ( x e. A \/ x e. B ) -> ( ( A < ( y e. C -> x
25	15 24	sylbi	|- ( x e. ( A u. B ) -> ( ( A < ( y e. C -> x
26	25	3imp21	|- ( ( ( A < x
27	5 7 12 14 26	ssltd	|- ( ( A < ( A u. B ) <