Metamath Proof Explorer

Definition df-slts

Description: Define the relation that holds iff one set of surreals completely precedes another. (Contributed by Scott Fenton, 7-Dec-2021)

Ref Expression
Assertion df-slts ⊢ ≪ s = a b | a ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ a ∀ y ∈ b x < s y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslts class ≪ s
1 va setvar a
2 vb setvar b
3 1 cv setvar a
4 csur class No
5 3 4 wss wff a ⊆ No
6 2 cv setvar b
7 6 4 wss wff b ⊆ No
8 vx setvar x
9 vy setvar y
10 8 cv setvar x
11 clts class < s
12 9 cv setvar y
13 10 12 11 wbr wff x < s y
14 13 9 6 wral wff ∀ y ∈ b x < s y
15 14 8 3 wral wff ∀ x ∈ a ∀ y ∈ b x < s y
16 5 7 15 w3a wff a ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ a ∀ y ∈ b x < s y
17 16 1 2 copab class a b | a ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ a ∀ y ∈ b x < s y
18 0 17 wceq wff ≪ s = a b | a ⊆ No ∧ b ⊆ No ∧ ∀ x ∈ a ∀ y ∈ b x < s y