Metamath Proof Explorer

Theorem ssslts1

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

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

Proof

Step Hyp Ref Expression
1 sltsex1 ⊢ A ≪ s B → A ∈ V
2 1 adantr ⊢ A ≪ s B ∧ C ⊆ A → A ∈ V
3 simpr ⊢ A ≪ s B ∧ C ⊆ A → C ⊆ A
4 2 3 ssexd ⊢ A ≪ s B ∧ C ⊆ A → C ∈ V
5 sltsex2 ⊢ A ≪ s B → B ∈ V
6 5 adantr ⊢ A ≪ s B ∧ C ⊆ A → B ∈ V
7 sltsss1 ⊢ A ≪ s B → A ⊆ No
8 7 adantr ⊢ A ≪ s B ∧ C ⊆ A → A ⊆ No
9 3 8 sstrd ⊢ A ≪ s B ∧ C ⊆ A → C ⊆ No
10 sltsss2 ⊢ A ≪ s B → B ⊆ No
11 10 adantr ⊢ A ≪ s B ∧ C ⊆ A → B ⊆ No
12 sltssep ⊢ A ≪ s B → ∀ x ∈ A ∀ y ∈ B x < s y
13 ssralv ⊢ C ⊆ A → ∀ x ∈ A ∀ y ∈ B x < s y → ∀ x ∈ C ∀ y ∈ B x < s y
14 12 13 mpan9 ⊢ A ≪ s B ∧ C ⊆ A → ∀ x ∈ C ∀ y ∈ B x < s y
15 9 11 14 3jca ⊢ A ≪ s B ∧ C ⊆ A → C ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ C ∀ y ∈ B x < s y
16 brslts ⊢ C ≪ s B ↔ C ∈ V ∧ B ∈ V ∧ C ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ C ∀ y ∈ B x < s y
17 4 6 15 16 syl21anbrc ⊢ A ≪ s B ∧ C ⊆ A → C ≪ s B