Description: The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | nulsslt | ⊢ ( 𝐴 ∈ 𝒫 No → ∅ <<s 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | ⊢ ( 𝐴 ∈ 𝒫 No → 𝐴 ∈ V ) | |
2 | 0ex | ⊢ ∅ ∈ V | |
3 | 1 2 | jctil | ⊢ ( 𝐴 ∈ 𝒫 No → ( ∅ ∈ V ∧ 𝐴 ∈ V ) ) |
4 | 0ss | ⊢ ∅ ⊆ No | |
5 | 4 | a1i | ⊢ ( 𝐴 ∈ 𝒫 No → ∅ ⊆ No ) |
6 | elpwi | ⊢ ( 𝐴 ∈ 𝒫 No → 𝐴 ⊆ No ) | |
7 | ral0 | ⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 | |
8 | 7 | a1i | ⊢ ( 𝐴 ∈ 𝒫 No → ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) |
9 | 5 6 8 | 3jca | ⊢ ( 𝐴 ∈ 𝒫 No → ( ∅ ⊆ No ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) ) |
10 | brsslt | ⊢ ( ∅ <<s 𝐴 ↔ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) ∧ ( ∅ ⊆ No ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) ) ) | |
11 | 3 9 10 | sylanbrc | ⊢ ( 𝐴 ∈ 𝒫 No → ∅ <<s 𝐴 ) |