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 ssltex1 ⊢ B ≪ s C → B ∈ V
3 unexg ⊢ A ∈ V ∧ B ∈ V → A ∪ B ∈ V
4 1 2 3 syl2an ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ∈ V
5 ssltex2 ⊢ A ≪ s C → C ∈ V
6 5 adantr ⊢ A ≪ s C ∧ B ≪ s C → C ∈ V
7 4 6 jca ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ∈ V ∧ 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 ⊢ B ≪ s C → C ⊆ No
14 13 adantl ⊢ A ≪ s C ∧ B ≪ s C → C ⊆ No
15 ssltsep ⊢ A ≪ s C → ∀ x ∈ A ∀ y ∈ C x < s y
16 15 adantr ⊢ A ≪ s C ∧ B ≪ s C → ∀ x ∈ A ∀ y ∈ C x < s y
17 ssltsep ⊢ B ≪ s C → ∀ x ∈ B ∀ y ∈ C x < s y
18 17 adantl ⊢ A ≪ s C ∧ B ≪ s C → ∀ x ∈ B ∀ y ∈ C x < s y
19 ralunb ⊢ ∀ x ∈ A ∪ B ∀ y ∈ C x < s y ↔ ∀ x ∈ A ∀ y ∈ C x < s y ∧ ∀ x ∈ B ∀ y ∈ C x < s y
20 16 18 19 sylanbrc ⊢ A ≪ s C ∧ B ≪ s C → ∀ x ∈ A ∪ B ∀ y ∈ C x < s y
21 12 14 20 3jca ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ⊆ No ∧ C ⊆ No ∧ ∀ x ∈ A ∪ B ∀ y ∈ C x < s y
22 brsslt ⊢ A ∪ B ≪ s C ↔ A ∪ B ∈ V ∧ C ∈ V ∧ A ∪ B ⊆ No ∧ C ⊆ No ∧ ∀ x ∈ A ∪ B ∀ y ∈ C x < s y
23 7 21 22 sylanbrc ⊢ A ≪ s C ∧ B ≪ s C → A ∪ B ≪ s C