Metamath Proof Explorer

Theorem sssslt2

Description: Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021)

Ref Expression
Assertion sssslt2 ⊢ A ≪ s B ∧ C ⊆ B → A ≪ s C

Proof

Step Hyp Ref Expression
1 ssltex1 ⊢ A ≪ s B → A ∈ V
2 1 adantr ⊢ A ≪ s B ∧ C ⊆ B → A ∈ V
3 ssltex2 ⊢ A ≪ s B → B ∈ V
4 3 adantr ⊢ A ≪ s B ∧ C ⊆ B → B ∈ V
5 simpr ⊢ A ≪ s B ∧ C ⊆ B → C ⊆ B
6 4 5 ssexd ⊢ A ≪ s B ∧ C ⊆ B → C ∈ V
7 ssltss1 ⊢ A ≪ s B → A ⊆ No
8 7 adantr ⊢ A ≪ s B ∧ C ⊆ B → A ⊆ No
9 ssltss2 ⊢ A ≪ s B → B ⊆ No
10 9 adantr ⊢ A ≪ s B ∧ C ⊆ B → B ⊆ No
11 5 10 sstrd ⊢ A ≪ s B ∧ C ⊆ B → C ⊆ No
12 ssltsep ⊢ A ≪ s B → ∀ x ∈ A ∀ y ∈ B x < s y
13 12 adantr ⊢ A ≪ s B ∧ C ⊆ B → ∀ x ∈ A ∀ y ∈ B x < s y
14 ssralv ⊢ C ⊆ B → ∀ y ∈ B x < s y → ∀ y ∈ C x < s y
15 5 14 syl ⊢ A ≪ s B ∧ C ⊆ B → ∀ y ∈ B x < s y → ∀ y ∈ C x < s y
16 15 ralimdv ⊢ A ≪ s B ∧ C ⊆ B → ∀ x ∈ A ∀ y ∈ B x < s y → ∀ x ∈ A ∀ y ∈ C x < s y
17 13 16 mpd ⊢ A ≪ s B ∧ C ⊆ B → ∀ x ∈ A ∀ y ∈ C x < s y
18 8 11 17 3jca ⊢ A ≪ s B ∧ C ⊆ B → A ⊆ No ∧ C ⊆ No ∧ ∀ x ∈ A ∀ y ∈ C x < s y
19 brsslt ⊢ A ≪ s C ↔ A ∈ V ∧ C ∈ V ∧ A ⊆ No ∧ C ⊆ No ∧ ∀ x ∈ A ∀ y ∈ C x < s y
20 2 6 18 19 syl21anbrc ⊢ A ≪ s B ∧ C ⊆ B → A ≪ s C