sltval

Description: The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011)

		Ref	Expression
	Assertion	sltval	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ f = A \to (f \in No \leftrightarrow A \in No)$
2	1	anbi1d	$⊢ f = A \to ((f \in No \land g \in No) \leftrightarrow (A \in No \land g \in No))$
3		fveq1	$⊢ f = A \to f (y) = A (y)$
4	3	eqeq1d	$⊢ f = A \to (f (y) = g (y) \leftrightarrow A (y) = g (y))$
5	4	ralbidv	$⊢ f = A \to (\forall y \in x f (y) = g (y) \leftrightarrow \forall y \in x A (y) = g (y))$
6		fveq1	$⊢ f = A \to f (x) = A (x)$
7	6	breq1d	$⊢ f = A \to (f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x) \leftrightarrow A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x))$
8	5 7	anbi12d	$⊢ f = A \to ((\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)) \leftrightarrow (\forall y \in x A (y) = g (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)))$
9	8	rexbidv	$⊢ f = A \to (\exists x \in On (\forall y \in x f (y) = g (y) \land f (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)) \leftrightarrow \exists x \in On (\forall y \in x A (y) = g (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)))$
10	2 9	anbi12d	$⊢ f = A \to (((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))) \leftrightarrow ((A \in No \land g \in No) \land \exists x \in On (\forall y \in x A (y) = g (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x))))$
11		eleq1	$⊢ g = B \to (g \in No \leftrightarrow B \in No)$
12	11	anbi2d	$⊢ g = B \to ((A \in No \land g \in No) \leftrightarrow (A \in No \land B \in No))$
13		fveq1	$⊢ g = B \to g (y) = B (y)$
14	13	eqeq2d	$⊢ g = B \to (A (y) = g (y) \leftrightarrow A (y) = B (y))$
15	14	ralbidv	$⊢ g = B \to (\forall y \in x A (y) = g (y) \leftrightarrow \forall y \in x A (y) = B (y))$
16		fveq1	$⊢ g = B \to g (x) = B (x)$
17	16	breq2d	$⊢ g = B \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x) \leftrightarrow A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
18	15 17	anbi12d	$⊢ g = B \to ((\forall y \in x A (y) = g (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)) \leftrightarrow (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$
19	18	rexbidv	$⊢ g = B \to (\exists x \in On (\forall y \in x A (y) = g (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x)) \leftrightarrow \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$
20	12 19	anbi12d	$⊢ g = B \to (((A \in No \land g \in No) \land \exists x \in On (\forall y \in x A (y) = g (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} g (x))) \leftrightarrow ((A \in No \land B \in No) \land \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))))$
21		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)))\}$
22	10 20 21	brabg	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow ((A \in No \land B \in No) \land \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))))$
23	22	bianabs	$⊢ (A \in No \land B \in No) \to (A <_{s} B \leftrightarrow \exists x \in On (\forall y \in x A (y) = B (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$

Metamath Proof Explorer

Theorem sltval

Proof