df-slt

Description: Next, we introduce surreal less-than, a comparison relation over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011)

		Ref	Expression
	Assertion	df-slt	$⊢ <_{s} = \{⟨f, g⟩ \| ((f \in No \land g \in No) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cslt	$class <_{s}$
1		vf	$setvar f$
2		vg	$setvar g$
3	1	cv	$setvar f$
4		csur	$class No$
5	3 4	wcel	$wff f \in No$
6	2	cv	$setvar g$
7	6 4	wcel	$wff g \in No$
8	5 7	wa	$wff (f \in No \land g \in No)$
9		vx	$setvar x$
10		con0	$class On$
11		vy	$setvar y$
12	9	cv	$setvar x$
13	11	cv	$setvar y$
14	13 3	cfv	$class f (y)$
15	13 6	cfv	$class g (y)$
16	14 15	wceq	$wff f (y) = g (y)$
17	16 11 12	wral	$wff \forall y \in x f (y) = g (y)$
18	12 3	cfv	$class f (x)$
19		c1o	$class 1_{𝑜}$
20		c0	$class \emptyset$
21	19 20	cop	$class ⟨1_{𝑜}, \emptyset⟩$
22		c2o	$class 2_{𝑜}$
23	19 22	cop	$class ⟨1_{𝑜}, 2_{𝑜}⟩$
24	20 22	cop	$class ⟨\emptyset, 2_{𝑜}⟩$
25	21 23 24	ctp	$class \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\}$
26	12 6	cfv	$class g (x)$
27	18 26 25	wbr	$wff f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)$
28	17 27	wa	$wff (\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x))$
29	28 9 10	wrex	$wff \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x))$
30	8 29	wa	$wff ((f \in No \land g \in No) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)))$
31	30 1 2	copab	$class \{⟨f, g⟩ \| ((f \in No \land g \in No) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)))\}$
32	0 31	wceq	$wff <_{s} = \{⟨f, g⟩ \| ((f \in No \land g \in No) \land \exists x \in On (\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)))\}$

Metamath Proof Explorer

Definition df-slt

Detailed syntax breakdown