Theorem ssltun2

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

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

Proof

Step	Hyp	Ref	Expression
1		ssltex1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
2	1	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐴 ∈ V )
3		ssltex2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
4		ssltex2	⊢ ( 𝐴 <<s 𝐶 → 𝐶 ∈ V )
5		unexg	⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
6	3 4 5	syl2an	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
7	2 6	jca	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝐴 ∈ V ∧ ( 𝐵 ∪ 𝐶 ) ∈ V ) )
8		ssltss1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
9	8	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐴 ⊆ No )
10		ssltss2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
11	10	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐵 ⊆ No )
12		ssltss2	⊢ ( 𝐴 <<s 𝐶 → 𝐶 ⊆ No )
13	12	adantl	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐶 ⊆ No )
14	11 13	unssd	⊢ ( ( 𝐴 <<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	19	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
21		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
22	20 21	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) 𝑥 <s 𝑦 ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
23	16 18 22	sylanbrc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) 𝑥 <s 𝑦 )
24	9 14 23	3jca	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → ( 𝐴 ⊆ No ∧ ( 𝐵 ∪ 𝐶 ) ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) 𝑥 <s 𝑦 ) )
25		brsslt	⊢ ( 𝐴 <<s ( 𝐵 ∪ 𝐶 ) ↔ ( ( 𝐴 ∈ V ∧ ( 𝐵 ∪ 𝐶 ) ∈ V ) ∧ ( 𝐴 ⊆ No ∧ ( 𝐵 ∪ 𝐶 ) ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) 𝑥 <s 𝑦 ) ) )
26	7 24 25	sylanbrc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶 ) → 𝐴 <<s ( 𝐵 ∪ 𝐶 ) )