Metamath Proof Explorer

Theorem nulsslt

Description: The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion nulsslt ⊢ A ∈ 𝒫 No → ∅ ≪ s A

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ 𝒫 No → A ∈ V
2 0ex ⊢ ∅ ∈ V
3 1 2 jctil ⊢ A ∈ 𝒫 No → ∅ ∈ V ∧ A ∈ V
4 0ss ⊢ ∅ ⊆ No
5 4 a1i ⊢ A ∈ 𝒫 No → ∅ ⊆ No
6 elpwi ⊢ A ∈ 𝒫 No → A ⊆ No
7 ral0 ⊢ ∀ x ∈ ∅ ∀ y ∈ A x < s y
8 7 a1i ⊢ A ∈ 𝒫 No → ∀ x ∈ ∅ ∀ y ∈ A x < s y
9 5 6 8 3jca ⊢ A ∈ 𝒫 No → ∅ ⊆ No ∧ A ⊆ No ∧ ∀ x ∈ ∅ ∀ y ∈ A x < s y
10 brsslt ⊢ ∅ ≪ s A ↔ ∅ ∈ V ∧ A ∈ V ∧ ∅ ⊆ No ∧ A ⊆ No ∧ ∀ x ∈ ∅ ∀ y ∈ A x < s y
11 3 9 10 sylanbrc ⊢ A ∈ 𝒫 No → ∅ ≪ s A