Theorem sltsun2

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

	Ref	Expression
Assertion	sltsun2	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐴 <<s ( 𝐵 ∪ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		sltsex1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
2	1	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐴 ∈ V )
3		sltsex2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
4	3	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐵 ∈ V )
5		sltsex2	⊢ ( 𝐴 <<s 𝐶 → 𝐶 ∈ V )
6	5	adantl	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐶 ∈ V )
7	4 6	unexd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
8		sltsss1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
9	8	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐴 ⊆ No )
10		sltsss2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
11	10	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐵 ⊆ No )
12		sltsss2	⊢ ( 𝐴 <<s 𝐶 → 𝐶 ⊆ No )
13	12	adantl	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐶 ⊆ No )
14	11 13	unssd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝐵 ∪ 𝐶 ) ⊆ No )
15		elun	⊢ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) )
16		sltssepc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 <s 𝑦 )
17	16	3exp	⊢ ( 𝐴 <<s 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑥 <s 𝑦 ) ) )
18	17	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑥 <s 𝑦 ) ) )
19	18	com3r	⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 <s 𝑦 ) ) )
20		sltssepc	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) → 𝑥 <s 𝑦 )
21	20	3exp	⊢ ( 𝐴 <<s 𝐶 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → 𝑥 <s 𝑦 ) ) )
22	21	adantl	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐶 → 𝑥 <s 𝑦 ) ) )
23	22	com3r	⊢ ( 𝑦 ∈ 𝐶 → ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 <s 𝑦 ) ) )
24	19 23	jaoi	⊢ ( ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) → ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 <s 𝑦 ) ) )
25	15 24	sylbi	⊢ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) → ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 <s 𝑦 ) ) )
26	25	3imp231	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ) → 𝑥 <s 𝑦 )
27	2 7 9 14 26	sltsd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐴 <<s ( 𝐵 ∪ 𝐶 ) )