Metamath Proof Explorer


Theorem ssltss2

Description: The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion ssltss2 ( 𝐴 <<s 𝐵𝐵 No )

Proof

Step Hyp Ref Expression
1 brsslt ( 𝐴 <<s 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐴 No 𝐵 No ∧ ∀ 𝑥𝐴𝑦𝐵 𝑥 <s 𝑦 ) ) )
2 simpr2 ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐴 No 𝐵 No ∧ ∀ 𝑥𝐴𝑦𝐵 𝑥 <s 𝑦 ) ) → 𝐵 No )
3 1 2 sylbi ( 𝐴 <<s 𝐵𝐵 No )