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 ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐴 <<s 𝐶 )

Proof

Step Hyp Ref Expression
1 ssltex1 ( 𝐴 <<s 𝐵𝐴 ∈ V )
2 1 adantr ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐴 ∈ V )
3 ssltex2 ( 𝐴 <<s 𝐵𝐵 ∈ V )
4 3 adantr ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐵 ∈ V )
5 simpr ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐶𝐵 )
6 4 5 ssexd ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐶 ∈ V )
7 ssltss1 ( 𝐴 <<s 𝐵𝐴 No )
8 7 adantr ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐴 No )
9 ssltss2 ( 𝐴 <<s 𝐵𝐵 No )
10 9 adantr ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐵 No )
11 5 10 sstrd ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐶 No )
12 ssltsep ( 𝐴 <<s 𝐵 → ∀ 𝑥𝐴𝑦𝐵 𝑥 <s 𝑦 )
13 ssralv ( 𝐶𝐵 → ( ∀ 𝑦𝐵 𝑥 <s 𝑦 → ∀ 𝑦𝐶 𝑥 <s 𝑦 ) )
14 13 ralimdv ( 𝐶𝐵 → ( ∀ 𝑥𝐴𝑦𝐵 𝑥 <s 𝑦 → ∀ 𝑥𝐴𝑦𝐶 𝑥 <s 𝑦 ) )
15 12 14 mpan9 ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → ∀ 𝑥𝐴𝑦𝐶 𝑥 <s 𝑦 )
16 8 11 15 3jca ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → ( 𝐴 No 𝐶 No ∧ ∀ 𝑥𝐴𝑦𝐶 𝑥 <s 𝑦 ) )
17 brsslt ( 𝐴 <<s 𝐶 ↔ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝐴 No 𝐶 No ∧ ∀ 𝑥𝐴𝑦𝐶 𝑥 <s 𝑦 ) ) )
18 2 6 16 17 syl21anbrc ( ( 𝐴 <<s 𝐵𝐶𝐵 ) → 𝐴 <<s 𝐶 )