Metamath Proof Explorer

Theorem ssltun2

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

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

Proof

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