Metamath Proof Explorer

Theorem sssslt1

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

Ref Expression
Assertion sssslt1 ⊢A≪sB∧C⊆A→C≪sB

Proof

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