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