dfn0s2

Description: Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

		Ref	Expression
	Assertion	dfn0s2	$⊢ ℕ_{0s} = ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$

Proof

Step	Hyp	Ref	Expression
1		0sno	$⊢ 0_{s} \in No$
2	1	elexi	$⊢ 0_{s} \in V$
3	2	elintab	$⊢ 0_{s} \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \leftrightarrow \forall x ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to 0_{s} \in x)$
4		simpl	$⊢ (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to 0_{s} \in x$
5	3 4	mpgbir	$⊢ 0_{s} \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$
6		oveq1	$⊢ y = z \to y +_{s} 1_{s} = z +_{s} 1_{s}$
7	6	eleq1d	$⊢ y = z \to (y +_{s} 1_{s} \in x \leftrightarrow z +_{s} 1_{s} \in x)$
8	7	rspccv	$⊢ \forall y \in x y +_{s} 1_{s} \in x \to (z \in x \to z +_{s} 1_{s} \in x)$
9	8	adantl	$⊢ (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to (z \in x \to z +_{s} 1_{s} \in x)$
10	9	a2i	$⊢ ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to z \in x) \to ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to z +_{s} 1_{s} \in x)$
11	10	alimi	$⊢ \forall x ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to z \in x) \to \forall x ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to z +_{s} 1_{s} \in x)$
12		vex	$⊢ z \in V$
13	12	elintab	$⊢ z \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \leftrightarrow \forall x ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to z \in x)$
14		ovex	$⊢ z +_{s} 1_{s} \in V$
15	14	elintab	$⊢ z +_{s} 1_{s} \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \leftrightarrow \forall x ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \to z +_{s} 1_{s} \in x)$
16	11 13 15	3imtr4i	$⊢ z \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \to z +_{s} 1_{s} \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$
17	16	rgen	$⊢ \forall z \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} z +_{s} 1_{s} \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$
18		peano5n0s	$⊢ (0_{s} \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \land \forall z \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} z +_{s} 1_{s} \in ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}) \to ℕ_{0s} \subseteq ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$
19	5 17 18	mp2an	$⊢ ℕ_{0s} \subseteq ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$
20		0n0s	$⊢ 0_{s} \in ℕ_{0s}$
21		peano2n0s	$⊢ y \in ℕ_{0s} \to y +_{s} 1_{s} \in ℕ_{0s}$
22	21	rgen	$⊢ \forall y \in ℕ_{0s} y +_{s} 1_{s} \in ℕ_{0s}$
23		n0sex	$⊢ ℕ_{0s} \in V$
24		eleq2	$⊢ x = ℕ_{0s} \to (0_{s} \in x \leftrightarrow 0_{s} \in ℕ_{0s})$
25		eleq2	$⊢ x = ℕ_{0s} \to (y +_{s} 1_{s} \in x \leftrightarrow y +_{s} 1_{s} \in ℕ_{0s})$
26	25	raleqbi1dv	$⊢ x = ℕ_{0s} \to (\forall y \in x y +_{s} 1_{s} \in x \leftrightarrow \forall y \in ℕ_{0s} y +_{s} 1_{s} \in ℕ_{0s})$
27	24 26	anbi12d	$⊢ x = ℕ_{0s} \to ((0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x) \leftrightarrow (0_{s} \in ℕ_{0s} \land \forall y \in ℕ_{0s} y +_{s} 1_{s} \in ℕ_{0s}))$
28	23 27	elab	$⊢ ℕ_{0s} \in \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \leftrightarrow (0_{s} \in ℕ_{0s} \land \forall y \in ℕ_{0s} y +_{s} 1_{s} \in ℕ_{0s})$
29	20 22 28	mpbir2an	$⊢ ℕ_{0s} \in \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$
30		intss1	$⊢ ℕ_{0s} \in \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \to ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \subseteq ℕ_{0s}$
31	29 30	ax-mp	$⊢ ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\} \subseteq ℕ_{0s}$
32	19 31	eqssi	$⊢ ℕ_{0s} = ⋂ \{x \| (0_{s} \in x \land \forall y \in x y +_{s} 1_{s} \in x)\}$

Metamath Proof Explorer

Theorem dfn0s2

Proof