noseqrdgfn

Description: The recursive definition generator on surreal sequences is a function. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	$⊢ φ \to C \in No$
	om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
	om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
	noseqrdg.1	$⊢ φ \to A \in V$
	noseqrdg.2	$⊢ φ \to R = {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
	noseqrdg.3	$⊢ φ \to S = ran R$
Assertion	noseqrdgfn	$⊢ φ \to S Fn Z$

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	$⊢ φ \to C \in No$
2		om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
3		om2noseq.3	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
4		noseqrdg.1	$⊢ φ \to A \in V$
5		noseqrdg.2	$⊢ φ \to R = {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}$
6		noseqrdg.3	$⊢ φ \to S = ran R$
7	6	eleq2d	$⊢ φ \to (z \in S \leftrightarrow z \in ran R)$
8		frfnom	$⊢ ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω$
9	5	fneq1d	$⊢ φ \to (R Fn ω \leftrightarrow ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x F y⟩), ⟨C, A⟩) ↾}_{ω}) Fn ω)$
10	8 9	mpbiri	$⊢ φ \to R Fn ω$
11		fvelrnb	$⊢ R Fn ω \to (z \in ran R \leftrightarrow \exists w \in ω R (w) = z)$
12	10 11	syl	$⊢ φ \to (z \in ran R \leftrightarrow \exists w \in ω R (w) = z)$
13	7 12	bitrd	$⊢ φ \to (z \in S \leftrightarrow \exists w \in ω R (w) = z)$
14	1 2 3 4 5	om2noseqrdg	$⊢ (φ \land w \in ω) \to R (w) = ⟨G (w), 2^{nd} (R (w))⟩$
15	1 2 3	om2noseqfo	$⊢ φ \to G : ω \underset{onto}{⟶} Z$
16		fof	$⊢ G : ω \underset{onto}{⟶} Z \to G : ω ⟶ Z$
17	15 16	syl	$⊢ φ \to G : ω ⟶ Z$
18	17	ffvelcdmda	$⊢ (φ \land w \in ω) \to G (w) \in Z$
19		fvex	$⊢ 2^{nd} (R (w)) \in V$
20		opelxpi	$⊢ (G (w) \in Z \land 2^{nd} (R (w)) \in V) \to ⟨G (w), 2^{nd} (R (w))⟩ \in (Z \times V)$
21	18 19 20	sylancl	$⊢ (φ \land w \in ω) \to ⟨G (w), 2^{nd} (R (w))⟩ \in (Z \times V)$
22	14 21	eqeltrd	$⊢ (φ \land w \in ω) \to R (w) \in (Z \times V)$
23		eleq1	$⊢ R (w) = z \to (R (w) \in (Z \times V) \leftrightarrow z \in (Z \times V))$
24	22 23	syl5ibcom	$⊢ (φ \land w \in ω) \to (R (w) = z \to z \in (Z \times V))$
25	24	rexlimdva	$⊢ φ \to (\exists w \in ω R (w) = z \to z \in (Z \times V))$
26	13 25	sylbid	$⊢ φ \to (z \in S \to z \in (Z \times V))$
27	26	ssrdv	$⊢ φ \to S \subseteq Z \times V$
28		relxp	$⊢ Rel (Z \times V)$
29		relss	$⊢ S \subseteq Z \times V \to (Rel (Z \times V) \to Rel S)$
30	27 28 29	mpisyl	$⊢ φ \to Rel S$
31	6	eleq2d	$⊢ φ \to (⟨v, z⟩ \in S \leftrightarrow ⟨v, z⟩ \in ran R)$
32		fvelrnb	$⊢ R Fn ω \to (⟨v, z⟩ \in ran R \leftrightarrow \exists w \in ω R (w) = ⟨v, z⟩)$
33	10 32	syl	$⊢ φ \to (⟨v, z⟩ \in ran R \leftrightarrow \exists w \in ω R (w) = ⟨v, z⟩)$
34	31 33	bitrd	$⊢ φ \to (⟨v, z⟩ \in S \leftrightarrow \exists w \in ω R (w) = ⟨v, z⟩)$
35	14	eqeq1d	$⊢ (φ \land w \in ω) \to (R (w) = ⟨v, z⟩ \leftrightarrow ⟨G (w), 2^{nd} (R (w))⟩ = ⟨v, z⟩)$
36	35	biimpd	$⊢ (φ \land w \in ω) \to (R (w) = ⟨v, z⟩ \to ⟨G (w), 2^{nd} (R (w))⟩ = ⟨v, z⟩)$
37	36	impr	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to ⟨G (w), 2^{nd} (R (w))⟩ = ⟨v, z⟩$
38		fvex	$⊢ G (w) \in V$
39	38 19	opth1	$⊢ ⟨G (w), 2^{nd} (R (w))⟩ = ⟨v, z⟩ \to G (w) = v$
40	37 39	syl	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to G (w) = v$
41	1 2 3	om2noseqf1o	$⊢ φ \to G : ω \underset{1-1 onto}{⟶} Z$
42		f1ocnvfv	$⊢ (G : ω \underset{1-1 onto}{⟶} Z \land w \in ω) \to (G (w) = v \to G^{-1} (v) = w)$
43	41 42	sylan	$⊢ (φ \land w \in ω) \to (G (w) = v \to G^{-1} (v) = w)$
44	43	adantrr	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to (G (w) = v \to G^{-1} (v) = w)$
45	40 44	mpd	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to G^{-1} (v) = w$
46	45	fveq2d	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to R (G^{-1} (v)) = R (w)$
47	46	fveq2d	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to 2^{nd} (R (G^{-1} (v))) = 2^{nd} (R (w))$
48		vex	$⊢ v \in V$
49		vex	$⊢ z \in V$
50	48 49	op2ndd	$⊢ R (w) = ⟨v, z⟩ \to 2^{nd} (R (w)) = z$
51	50	ad2antll	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to 2^{nd} (R (w)) = z$
52	47 51	eqtr2d	$⊢ (φ \land (w \in ω \land R (w) = ⟨v, z⟩)) \to z = 2^{nd} (R (G^{-1} (v)))$
53	52	rexlimdvaa	$⊢ φ \to (\exists w \in ω R (w) = ⟨v, z⟩ \to z = 2^{nd} (R (G^{-1} (v))))$
54	34 53	sylbid	$⊢ φ \to (⟨v, z⟩ \in S \to z = 2^{nd} (R (G^{-1} (v))))$
55	54	alrimiv	$⊢ φ \to \forall z (⟨v, z⟩ \in S \to z = 2^{nd} (R (G^{-1} (v))))$
56		fvex	$⊢ 2^{nd} (R (G^{-1} (v))) \in V$
57		eqeq2	$⊢ w = 2^{nd} (R (G^{-1} (v))) \to (z = w \leftrightarrow z = 2^{nd} (R (G^{-1} (v))))$
58	57	imbi2d	$⊢ w = 2^{nd} (R (G^{-1} (v))) \to ((⟨v, z⟩ \in S \to z = w) \leftrightarrow (⟨v, z⟩ \in S \to z = 2^{nd} (R (G^{-1} (v)))))$
59	58	albidv	$⊢ w = 2^{nd} (R (G^{-1} (v))) \to (\forall z (⟨v, z⟩ \in S \to z = w) \leftrightarrow \forall z (⟨v, z⟩ \in S \to z = 2^{nd} (R (G^{-1} (v)))))$
60	56 59	spcev	$⊢ \forall z (⟨v, z⟩ \in S \to z = 2^{nd} (R (G^{-1} (v)))) \to \exists w \forall z (⟨v, z⟩ \in S \to z = w)$
61	55 60	syl	$⊢ φ \to \exists w \forall z (⟨v, z⟩ \in S \to z = w)$
62	61	alrimiv	$⊢ φ \to \forall v \exists w \forall z (⟨v, z⟩ \in S \to z = w)$
63		dffun5	$⊢ Fun S \leftrightarrow (Rel S \land \forall v \exists w \forall z (⟨v, z⟩ \in S \to z = w))$
64	30 62 63	sylanbrc	$⊢ φ \to Fun S$
65		dmss	$⊢ S \subseteq Z \times V \to dom S \subseteq dom (Z \times V)$
66	27 65	syl	$⊢ φ \to dom S \subseteq dom (Z \times V)$
67		dmxpss	$⊢ dom (Z \times V) \subseteq Z$
68	66 67	sstrdi	$⊢ φ \to dom S \subseteq Z$
69	1 2 3 4 5	noseqrdglem	$⊢ (φ \land v \in Z) \to ⟨v, 2^{nd} (R (G^{-1} (v)))⟩ \in ran R$
70	6	adantr	$⊢ (φ \land v \in Z) \to S = ran R$
71	69 70	eleqtrrd	$⊢ (φ \land v \in Z) \to ⟨v, 2^{nd} (R (G^{-1} (v)))⟩ \in S$
72	48 56	opeldm	$⊢ ⟨v, 2^{nd} (R (G^{-1} (v)))⟩ \in S \to v \in dom S$
73	71 72	syl	$⊢ (φ \land v \in Z) \to v \in dom S$
74	68 73	eqelssd	$⊢ φ \to dom S = Z$
75		df-fn	$⊢ S Fn Z \leftrightarrow (Fun S \land dom S = Z)$
76	64 74 75	sylanbrc	$⊢ φ \to S Fn Z$

Metamath Proof Explorer

Theorem noseqrdgfn

Proof