Metamath Proof Explorer

Theorem ssslts2

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

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

Proof

Step Hyp Ref Expression
1 sltsex1 ⊢ A ≪ s B → A ∈ V
2 1 adantr ⊢ A ≪ s B ∧ C ⊆ B → A ∈ V
3 sltsex2 ⊢ 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 sltsss1 ⊢ A ≪ s B → A ⊆ No
8 7 adantr ⊢ A ≪ s B ∧ C ⊆ B → A ⊆ No
9 sltsss2 ⊢ 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 sltssep ⊢ A ≪ s B → ∀ x ∈ A ∀ y ∈ B x < s y
13 ssralv ⊢ C ⊆ B → ∀ y ∈ B x < s y → ∀ y ∈ C x < s y
14 13 ralimdv ⊢ C ⊆ B → ∀ x ∈ A ∀ y ∈ B x < s y → ∀ x ∈ A ∀ y ∈ C x < s y
15 12 14 mpan9 ⊢ A ≪ s B ∧ C ⊆ B → ∀ x ∈ A ∀ y ∈ C x < s y
16 8 11 15 3jca ⊢ A ≪ s B ∧ C ⊆ B → A ⊆ No ∧ C ⊆ No ∧ ∀ x ∈ A ∀ y ∈ C x < s y
17 brslts ⊢ A ≪ s C ↔ A ∈ V ∧ C ∈ V ∧ A ⊆ No ∧ C ⊆ No ∧ ∀ x ∈ A ∀ y ∈ C x < s y
18 2 6 16 17 syl21anbrc ⊢ A ≪ s B ∧ C ⊆ B → A ≪ s C