noseqind

Description: Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	noseq.1	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω]$
	noseq.2	$⊢ φ \to A \in No$
	noseqind.3	$⊢ φ \to A \in B$
	noseqind.4	$⊢ (φ \land y \in B) \to y +_{s} 1_{s} \in B$
Assertion	noseqind	$⊢ φ \to Z \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		noseq.1	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω]$
2		noseq.2	$⊢ φ \to A \in No$
3		noseqind.3	$⊢ φ \to A \in B$
4		noseqind.4	$⊢ (φ \land y \in B) \to y +_{s} 1_{s} \in B$
5		df-ima	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω] = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
6	1 5	eqtrdi	$⊢ φ \to Z = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω})$
7		fveq2	$⊢ z = \emptyset \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (\emptyset)$
8	7	eleq1d	$⊢ z = \emptyset \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (\emptyset) \in B)$
9		fveq2	$⊢ z = w \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w)$
10	9	eleq1d	$⊢ z = w \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \in B)$
11		fveq2	$⊢ z = suc w \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc w)$
12	11	eleq1d	$⊢ z = suc w \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc w) \in B)$
13		fr0g	$⊢ A \in No \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (\emptyset) = A$
14	2 13	syl	$⊢ φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (\emptyset) = A$
15	14 3	eqeltrd	$⊢ φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (\emptyset) \in B$
16		oveq1	$⊢ y = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \to y +_{s} 1_{s} = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s}$
17	16	eleq1d	$⊢ y = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \to (y +_{s} 1_{s} \in B \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s} \in B)$
18	17	imbi2d	$⊢ y = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \to ((φ \to y +_{s} 1_{s} \in B) \leftrightarrow (φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s} \in B))$
19	4	expcom	$⊢ y \in B \to (φ \to y +_{s} 1_{s} \in B)$
20	18 19	vtoclga	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \in B \to (φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s} \in B)$
21	20	impcom	$⊢ (φ \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \in B) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s} \in B$
22		ovex	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s} \in V$
23		eqid	$⊢ {rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω} = {rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}$
24		oveq1	$⊢ t = x \to t +_{s} 1_{s} = x +_{s} 1_{s}$
25		oveq1	$⊢ t = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \to t +_{s} 1_{s} = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s}$
26	23 24 25	frsucmpt2	$⊢ (w \in ω \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s} \in V) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc w) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s}$
27	22 26	mpan2	$⊢ w \in ω \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc w) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s}$
28	27	eleq1d	$⊢ w \in ω \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc w) \in B \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) +_{s} 1_{s} \in B)$
29	21 28	imbitrrid	$⊢ w \in ω \to ((φ \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \in B) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc w) \in B)$
30	29	expd	$⊢ w \in ω \to (φ \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (w) \in B \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (suc w) \in B))$
31	8 10 12 15 30	finds2	$⊢ z \in ω \to (φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B)$
32	31	com12	$⊢ φ \to (z \in ω \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B)$
33	32	ralrimiv	$⊢ φ \to \forall z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B$
34		frfnom	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) Fn ω$
35		ffnfv	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) : ω ⟶ B \leftrightarrow (({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) Fn ω \land \forall z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B)$
36	34 35	mpbiran	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) : ω ⟶ B \leftrightarrow \forall z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) (z) \in B$
37	33 36	sylibr	$⊢ φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) : ω ⟶ B$
38	37	frnd	$⊢ φ \to ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), A) ↾}_{ω}) \subseteq B$
39	6 38	eqsstrd	$⊢ φ \to Z \subseteq B$

Metamath Proof Explorer

Theorem noseqind

Proof