0lt1s

Description: Surreal zero is less than surreal one. Theorem from Conway p. 7. (Contributed by Scott Fenton, 7-Aug-2024)

		Ref	Expression
	Assertion	0lt1s	$⊢ 0_{s} <_{s} 1_{s}$

Proof

Step	Hyp	Ref	Expression
1		0no	$⊢ 0_{s} \in No$
2		lesid	$⊢ 0_{s} \in No \to 0_{s} \leq_{s} 0_{s}$
3	1 2	ax-mp	$⊢ 0_{s} \leq_{s} 0_{s}$
4	1	elexi	$⊢ 0_{s} \in V$
5		breq2	$⊢ x = 0_{s} \to (0_{s} \leq_{s} x \leftrightarrow 0_{s} \leq_{s} 0_{s})$
6	4 5	rexsn	$⊢ \exists x \in \{0_{s}\} 0_{s} \leq_{s} x \leftrightarrow 0_{s} \leq_{s} 0_{s}$
7	3 6	mpbir	$⊢ \exists x \in \{0_{s}\} 0_{s} \leq_{s} x$
8	7	orci	$⊢ (\exists x \in \{0_{s}\} 0_{s} \leq_{s} x \lor \exists y \in \emptyset y \leq_{s} 1_{s})$
9		0elpw	$⊢ \emptyset \in 𝒫 No$
10		nulsgts	$⊢ \emptyset \in 𝒫 No \to \emptyset ≪_{s} \emptyset$
11	9 10	ax-mp	$⊢ \emptyset ≪_{s} \emptyset$
12		snssi	$⊢ 0_{s} \in No \to \{0_{s}\} \subseteq No$
13	1 12	ax-mp	$⊢ \{0_{s}\} \subseteq No$
14		snex	$⊢ \{0_{s}\} \in V$
15	14	elpw	$⊢ \{0_{s}\} \in 𝒫 No \leftrightarrow \{0_{s}\} \subseteq No$
16	13 15	mpbir	$⊢ \{0_{s}\} \in 𝒫 No$
17		nulsgts	$⊢ \{0_{s}\} \in 𝒫 No \to \{0_{s}\} ≪_{s} \emptyset$
18	16 17	ax-mp	$⊢ \{0_{s}\} ≪_{s} \emptyset$
19		df-0s	$⊢ 0_{s} = \emptyset \|_{s} \emptyset$
20		df-1s	$⊢ 1_{s} = \{0_{s}\} \|_{s} \emptyset$
21		ltsrec	$⊢ ((\emptyset ≪_{s} \emptyset \land \{0_{s}\} ≪_{s} \emptyset) \land (0_{s} = \emptyset \|_{s} \emptyset \land 1_{s} = \{0_{s}\} \|_{s} \emptyset)) \to (0_{s} <_{s} 1_{s} \leftrightarrow (\exists x \in \{0_{s}\} 0_{s} \leq_{s} x \lor \exists y \in \emptyset y \leq_{s} 1_{s}))$
22	11 18 19 20 21	mp4an	$⊢ 0_{s} <_{s} 1_{s} \leftrightarrow (\exists x \in \{0_{s}\} 0_{s} \leq_{s} x \lor \exists y \in \emptyset y \leq_{s} 1_{s})$
23	8 22	mpbir	$⊢ 0_{s} <_{s} 1_{s}$

Metamath Proof Explorer

Theorem 0lt1s

Proof