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