Theorem sltsun1

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

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

Proof

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