Metamath Proof Explorer

Theorem ssltsnb

Description: Surreal set less-than of two singletons. (Contributed by Scott Fenton, 18-Jan-2026)

Ref Expression
Hypotheses ssltsnb.1 ⊢ φ → A ∈ No
ssltsnb.2 ⊢ φ → B ∈ No
Assertion ssltsnb ⊢ φ → A ≪ s B ↔ A < s B

Proof

Step Hyp Ref Expression
1 ssltsnb.1 ⊢ φ → A ∈ No
2 ssltsnb.2 ⊢ φ → B ∈ No
3 snex ⊢ A ∈ V
4 snex ⊢ B ∈ V
5 3 4 pm3.2i ⊢ A ∈ V ∧ B ∈ V
6 brsslt ⊢ A ≪ s B ↔ A ∈ V ∧ B ∈ V ∧ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
7 5 6 mpbiran ⊢ A ≪ s B ↔ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
8 df-3an ⊢ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y ↔ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
9 breq1 ⊢ x = A → x < s y ↔ A < s y
10 9 ralbidv ⊢ x = A → ∀ y ∈ B x < s y ↔ ∀ y ∈ B A < s y
11 10 ralsng ⊢ A ∈ No → ∀ x ∈ A ∀ y ∈ B x < s y ↔ ∀ y ∈ B A < s y
12 1 11 syl ⊢ φ → ∀ x ∈ A ∀ y ∈ B x < s y ↔ ∀ y ∈ B A < s y
13 1 snssd ⊢ φ → A ⊆ No
14 2 snssd ⊢ φ → B ⊆ No
15 13 14 jca ⊢ φ → A ⊆ No ∧ B ⊆ No
16 15 biantrurd ⊢ φ → ∀ x ∈ A ∀ y ∈ B x < s y ↔ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
17 breq2 ⊢ y = B → A < s y ↔ A < s B
18 17 ralsng ⊢ B ∈ No → ∀ y ∈ B A < s y ↔ A < s B
19 2 18 syl ⊢ φ → ∀ y ∈ B A < s y ↔ A < s B
20 12 16 19 3bitr3d ⊢ φ → A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y ↔ A < s B
21 8 20 bitr2id ⊢ φ → A < s B ↔ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
22 7 21 bitr4id ⊢ φ → A ≪ s B ↔ A < s B