Theorem noseqrdgfn

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

	Ref	Expression
Hypotheses	om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
	om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
	om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
	noseqrdg.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	noseqrdg.2	⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
	noseqrdg.3	⊢ ( 𝜑 → 𝑆 = ran 𝑅 )
Assertion	noseqrdgfn	⊢ ( 𝜑 → 𝑆 Fn 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
2		om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3		om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4		noseqrdg.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		noseqrdg.2	⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
6		noseqrdg.3	⊢ ( 𝜑 → 𝑆 = ran 𝑅 )
7	6	eleq2d	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑆 ↔ 𝑧 ∈ ran 𝑅 ) )
8		frfnom	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω
9	5	fneq1d	⊢ ( 𝜑 → ( 𝑅 Fn ω ↔ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω ) )
10	8 9	mpbiri	⊢ ( 𝜑 → 𝑅 Fn ω )
11		fvelrnb	⊢ ( 𝑅 Fn ω → ( 𝑧 ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 ) )
12	10 11	syl	⊢ ( 𝜑 → ( 𝑧 ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 ) )
13	7 12	bitrd	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑆 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 ) )
14	1 2 3 4 5	om2noseqrdg	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ( 𝑅 ‘ 𝑤 ) = ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ )
15	1 2 3	om2noseqfo	⊢ ( 𝜑 → 𝐺 : ω –onto→ 𝑍 )
16		fof	⊢ ( 𝐺 : ω –onto→ 𝑍 → 𝐺 : ω ⟶ 𝑍 )
17	15 16	syl	⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝑍 )
18	17	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑍 )
19		fvex	⊢ ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ∈ V
20		opelxpi	⊢ ( ( ( 𝐺 ‘ 𝑤 ) ∈ 𝑍 ∧ ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ∈ V ) → ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ ∈ ( 𝑍 × V ) )
21	18 19 20	sylancl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ ∈ ( 𝑍 × V ) )
22	14 21	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ( 𝑅 ‘ 𝑤 ) ∈ ( 𝑍 × V ) )
23		eleq1	⊢ ( ( 𝑅 ‘ 𝑤 ) = 𝑧 → ( ( 𝑅 ‘ 𝑤 ) ∈ ( 𝑍 × V ) ↔ 𝑧 ∈ ( 𝑍 × V ) ) )
24	22 23	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ( ( 𝑅 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ ( 𝑍 × V ) ) )
25	24	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ ( 𝑍 × V ) ) )
26	13 25	sylbid	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ( 𝑍 × V ) ) )
27	26	ssrdv	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑍 × V ) )
28		relxp	⊢ Rel ( 𝑍 × V )
29		relss	⊢ ( 𝑆 ⊆ ( 𝑍 × V ) → ( Rel ( 𝑍 × V ) → Rel 𝑆 ) )
30	27 28 29	mpisyl	⊢ ( 𝜑 → Rel 𝑆 )
31	6	eleq2d	⊢ ( 𝜑 → ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 ↔ ⟨ 𝑣 , 𝑧 ⟩ ∈ ran 𝑅 ) )
32		fvelrnb	⊢ ( 𝑅 Fn ω → ( ⟨ 𝑣 , 𝑧 ⟩ ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) )
33	10 32	syl	⊢ ( 𝜑 → ( ⟨ 𝑣 , 𝑧 ⟩ ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) )
34	31 33	bitrd	⊢ ( 𝜑 → ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) )
35	14	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ↔ ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ = ⟨ 𝑣 , 𝑧 ⟩ ) )
36	35	biimpd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ = ⟨ 𝑣 , 𝑧 ⟩ ) )
37	36	impr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ = ⟨ 𝑣 , 𝑧 ⟩ )
38		fvex	⊢ ( 𝐺 ‘ 𝑤 ) ∈ V
39	38 19	opth1	⊢ ( ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ = ⟨ 𝑣 , 𝑧 ⟩ → ( 𝐺 ‘ 𝑤 ) = 𝑣 )
40	37 39	syl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → ( 𝐺 ‘ 𝑤 ) = 𝑣 )
41	1 2 3	om2noseqf1o	⊢ ( 𝜑 → 𝐺 : ω –1-1-onto→ 𝑍 )
42		f1ocnvfv	⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ 𝑤 ∈ ω ) → ( ( 𝐺 ‘ 𝑤 ) = 𝑣 → ( ◡ 𝐺 ‘ 𝑣 ) = 𝑤 ) )
43	41 42	sylan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ω ) → ( ( 𝐺 ‘ 𝑤 ) = 𝑣 → ( ◡ 𝐺 ‘ 𝑣 ) = 𝑤 ) )
44	43	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → ( ( 𝐺 ‘ 𝑤 ) = 𝑣 → ( ◡ 𝐺 ‘ 𝑣 ) = 𝑤 ) )
45	40 44	mpd	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → ( ◡ 𝐺 ‘ 𝑣 ) = 𝑤 )
46	45	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) = ( 𝑅 ‘ 𝑤 ) )
47	46	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) = ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) )
48		vex	⊢ 𝑣 ∈ V
49		vex	⊢ 𝑧 ∈ V
50	48 49	op2ndd	⊢ ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) = 𝑧 )
51	50	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → ( 2nd ‘ ( 𝑅 ‘ 𝑤 ) ) = 𝑧 )
52	47 51	eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) ) → 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) )
53	52	rexlimdvaa	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ) )
54	34 53	sylbid	⊢ ( 𝜑 → ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ) )
55	54	alrimiv	⊢ ( 𝜑 → ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ) )
56		fvex	⊢ ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ∈ V
57		eqeq2	⊢ ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) → ( 𝑧 = 𝑤 ↔ 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ) )
58	57	imbi2d	⊢ ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) → ( ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) ↔ ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ) ) )
59	58	albidv	⊢ ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) → ( ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) ↔ ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ) ) )
60	56 59	spcev	⊢ ( ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ) → ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) )
61	55 60	syl	⊢ ( 𝜑 → ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) )
62	61	alrimiv	⊢ ( 𝜑 → ∀ 𝑣 ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) )
63		dffun5	⊢ ( Fun 𝑆 ↔ ( Rel 𝑆 ∧ ∀ 𝑣 ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) ) )
64	30 62 63	sylanbrc	⊢ ( 𝜑 → Fun 𝑆 )
65		dmss	⊢ ( 𝑆 ⊆ ( 𝑍 × V ) → dom 𝑆 ⊆ dom ( 𝑍 × V ) )
66	27 65	syl	⊢ ( 𝜑 → dom 𝑆 ⊆ dom ( 𝑍 × V ) )
67		dmxpss	⊢ dom ( 𝑍 × V ) ⊆ 𝑍
68	66 67	sstrdi	⊢ ( 𝜑 → dom 𝑆 ⊆ 𝑍 )
69	1 2 3 4 5	noseqrdglem	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑍 ) → ⟨ 𝑣 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ⟩ ∈ ran 𝑅 )
70	6	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑍 ) → 𝑆 = ran 𝑅 )
71	69 70	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑍 ) → ⟨ 𝑣 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ⟩ ∈ 𝑆 )
72	48 56	opeldm	⊢ ( ⟨ 𝑣 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝑣 ) ) ) ⟩ ∈ 𝑆 → 𝑣 ∈ dom 𝑆 )
73	71 72	syl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑍 ) → 𝑣 ∈ dom 𝑆 )
74	68 73	eqelssd	⊢ ( 𝜑 → dom 𝑆 = 𝑍 )
75		df-fn	⊢ ( 𝑆 Fn 𝑍 ↔ ( Fun 𝑆 ∧ dom 𝑆 = 𝑍 ) )
76	64 74 75	sylanbrc	⊢ ( 𝜑 → 𝑆 Fn 𝑍 )