Theorem ssltun1

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

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

Proof

Step	Hyp	Ref	Expression
1		ssltex1	⊢ ( 𝐴 <<s 𝐶 → 𝐴 ∈ V )
2		ssltex1	⊢ ( 𝐵 <<s 𝐶 → 𝐵 ∈ V )
3		unexg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
4	1 2 3	syl2an	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
5		ssltex2	⊢ ( 𝐴 <<s 𝐶 → 𝐶 ∈ V )
6	5	adantr	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → 𝐶 ∈ V )
7	4 6	jca	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ( ( 𝐴 ∪ 𝐵 ) ∈ V ∧ 𝐶 ∈ V ) )
8		ssltss1	⊢ ( 𝐴 <<s 𝐶 → 𝐴 ⊆ No )
9	8	adantr	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → 𝐴 ⊆ No )
10		ssltss1	⊢ ( 𝐵 <<s 𝐶 → 𝐵 ⊆ No )
11	10	adantl	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → 𝐵 ⊆ No )
12	9 11	unssd	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ( 𝐴 ∪ 𝐵 ) ⊆ No )
13		ssltss2	⊢ ( 𝐵 <<s 𝐶 → 𝐶 ⊆ No )
14	13	adantl	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → 𝐶 ⊆ No )
15		ssltsep	⊢ ( 𝐴 <<s 𝐶 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 )
16	15	adantr	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 )
17		ssltsep	⊢ ( 𝐵 <<s 𝐶 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 )
18	17	adantl	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 )
19		ralunb	⊢ ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
20	16 18 19	sylanbrc	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 )
21	12 14 20	3jca	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ No ∧ 𝐶 ⊆ No ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
22		brsslt	⊢ ( ( 𝐴 ∪ 𝐵 ) <<s 𝐶 ↔ ( ( ( 𝐴 ∪ 𝐵 ) ∈ V ∧ 𝐶 ∈ V ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊆ No ∧ 𝐶 ⊆ No ∧ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) ) )
23	7 21 22	sylanbrc	⊢ ( ( 𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶 ) → ( 𝐴 ∪ 𝐵 ) <<s 𝐶 )