Metamath Proof Explorer

Theorem ssltun1

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

Ref Expression
Assertion ssltun1 ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ≪ s C

Proof

Step Hyp Ref Expression
1 ssltex1 ⊢ A ≪ s C → A ∈ V
2 1 adantr ⊢ A ≪ s C ∧ B ≪ s C → A ∈ V
3 ssltex1 ⊢ B ≪ s C → B ∈ V
4 3 adantl ⊢ A ≪ s C ∧ B ≪ s C → B ∈ V
5 2 4 unexd ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ∈ V
6 ssltex2 ⊢ A ≪ s C → C ∈ V
7 6 adantr ⊢ A ≪ s C ∧ B ≪ s C → C ∈ V
8 ssltss1 ⊢ A ≪ s C → A ⊆ No
9 8 adantr ⊢ A ≪ s C ∧ B ≪ s C → A ⊆ No
10 ssltss1 ⊢ B ≪ s C → B ⊆ No
11 10 adantl ⊢ A ≪ s C ∧ B ≪ s C → B ⊆ No
12 9 11 unssd ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ⊆ No
13 ssltss2 ⊢ A ≪ s C → C ⊆ No
14 13 adantr ⊢ A ≪ s C ∧ B ≪ s C → C ⊆ No
15 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
16 ssltsepc ⊢ A ≪ s C ∧ x ∈ A ∧ y ∈ C → x < s y
17 16 3exp ⊢ A ≪ s C → x ∈ A → y ∈ C → x < s y
18 17 adantr ⊢ A ≪ s C ∧ B ≪ s C → x ∈ A → y ∈ C → x < s y
19 18 com12 ⊢ x ∈ A → A ≪ s C ∧ B ≪ s C → y ∈ C → x < s y
20 ssltsepc ⊢ B ≪ s C ∧ x ∈ B ∧ y ∈ C → x < s y
21 20 3exp ⊢ B ≪ s C → x ∈ B → y ∈ C → x < s y
22 21 adantl ⊢ A ≪ s C ∧ B ≪ s C → x ∈ B → y ∈ C → x < s y
23 22 com12 ⊢ x ∈ B → A ≪ s C ∧ B ≪ s C → y ∈ C → x < s y
24 19 23 jaoi ⊢ x ∈ A ∨ x ∈ B → A ≪ s C ∧ B ≪ s C → y ∈ C → x < s y
25 15 24 sylbi ⊢ x ∈ A ∪ B → A ≪ s C ∧ B ≪ s C → y ∈ C → x < s y
26 25 3imp21 ⊢ A ≪ s C ∧ B ≪ s C ∧ x ∈ A ∪ B ∧ y ∈ C → x < s y
27 5 7 12 14 26 ssltd ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ≪ s C