Metamath Proof Explorer

Theorem sssslt2

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

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

Proof

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