uzrdgfni

Description: The recursive definition generator on upper integers is a function. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 4-May-2015)

	Ref	Expression
Hypotheses	om2uz.1	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
	uzrdg.1	⊢ 𝐴 ∈ V
	uzrdg.2	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
	uzrdg.3	⊢ 𝑆 = ran 𝑅
Assertion	uzrdgfni	⊢ 𝑆 Fn ( ℤ_≥ ‘ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	⊢ 𝐶 ∈ ℤ
2		om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3		uzrdg.1	⊢ 𝐴 ∈ V
4		uzrdg.2	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
5		uzrdg.3	⊢ 𝑆 = ran 𝑅
6	5	eleq2i	⊢ ( 𝑧 ∈ 𝑆 ↔ 𝑧 ∈ ran 𝑅 )
7		frfnom	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω
8	4	fneq1i	⊢ ( 𝑅 Fn ω ↔ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) Fn ω )
9	7 8	mpbir	⊢ 𝑅 Fn ω
10		fvelrnb	⊢ ( 𝑅 Fn ω → ( 𝑧 ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 ) )
11	9 10	ax-mp	⊢ ( 𝑧 ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 )
12	6 11	bitri	⊢ ( 𝑧 ∈ 𝑆 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 )
13	1 2 3 4	om2uzrdg	⊢ ( 𝑤 ∈ ω → ( 𝑅 ‘ 𝑤 ) = ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ )
14	1 2	om2uzuzi	⊢ ( 𝑤 ∈ ω → ( 𝐺 ‘ 𝑤 ) ∈ ( ℤ_≥ ‘ 𝐶 ) )
15		fvex	⊢ ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ∈ V
16		opelxpi	⊢ ( ( ( 𝐺 ‘ 𝑤 ) ∈ ( ℤ_≥ ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ∈ V ) → ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) )
17	14 15 16	sylancl	⊢ ( 𝑤 ∈ ω → ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) )
18	13 17	eqeltrd	⊢ ( 𝑤 ∈ ω → ( 𝑅 ‘ 𝑤 ) ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) )
19		eleq1	⊢ ( ( 𝑅 ‘ 𝑤 ) = 𝑧 → ( ( 𝑅 ‘ 𝑤 ) ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) ↔ 𝑧 ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) ) )
20	18 19	syl5ibcom	⊢ ( 𝑤 ∈ ω → ( ( 𝑅 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) ) )
21	20	rexlimiv	⊢ ( ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) )
22	12 21	sylbi	⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ( ( ℤ_≥ ‘ 𝐶 ) × V ) )
23	22	ssriv	⊢ 𝑆 ⊆ ( ( ℤ_≥ ‘ 𝐶 ) × V )
24		xpss	⊢ ( ( ℤ_≥ ‘ 𝐶 ) × V ) ⊆ ( V × V )
25	23 24	sstri	⊢ 𝑆 ⊆ ( V × V )
26		df-rel	⊢ ( Rel 𝑆 ↔ 𝑆 ⊆ ( V × V ) )
27	25 26	mpbir	⊢ Rel 𝑆
28		fvex	⊢ ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ∈ V
29		eqeq2	⊢ ( 𝑤 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) → ( 𝑧 = 𝑤 ↔ 𝑧 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ) )
30	29	imbi2d	⊢ ( 𝑤 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) → ( ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) ↔ ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ) ) )
31	30	albidv	⊢ ( 𝑤 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) → ( ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) ↔ ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ) ) )
32	28 31	spcev	⊢ ( ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ) → ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) )
33	5	eleq2i	⊢ ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 ↔ ⟨ 𝑣 , 𝑧 ⟩ ∈ ran 𝑅 )
34		fvelrnb	⊢ ( 𝑅 Fn ω → ( ⟨ 𝑣 , 𝑧 ⟩ ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) )
35	9 34	ax-mp	⊢ ( ⟨ 𝑣 , 𝑧 ⟩ ∈ ran 𝑅 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ )
36	33 35	bitri	⊢ ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 ↔ ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ )
37	13	eqeq1d	⊢ ( 𝑤 ∈ ω → ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ↔ ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ = ⟨ 𝑣 , 𝑧 ⟩ ) )
38		fvex	⊢ ( 𝐺 ‘ 𝑤 ) ∈ V
39	38 15	opth1	⊢ ( ⟨ ( 𝐺 ‘ 𝑤 ) , ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ⟩ = ⟨ 𝑣 , 𝑧 ⟩ → ( 𝐺 ‘ 𝑤 ) = 𝑣 )
40	37 39	biimtrdi	⊢ ( 𝑤 ∈ ω → ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → ( 𝐺 ‘ 𝑤 ) = 𝑣 ) )
41	1 2	om2uzf1oi	⊢ 𝐺 : ω –1-1-onto→ ( ℤ_≥ ‘ 𝐶 )
42		f1ocnvfv	⊢ ( ( 𝐺 : ω –1-1-onto→ ( ℤ_≥ ‘ 𝐶 ) ∧ 𝑤 ∈ ω ) → ( ( 𝐺 ‘ 𝑤 ) = 𝑣 → ( ^◡ 𝐺 ‘ 𝑣 ) = 𝑤 ) )
43	41 42	mpan	⊢ ( 𝑤 ∈ ω → ( ( 𝐺 ‘ 𝑤 ) = 𝑣 → ( ^◡ 𝐺 ‘ 𝑣 ) = 𝑤 ) )
44	40 43	syld	⊢ ( 𝑤 ∈ ω → ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → ( ^◡ 𝐺 ‘ 𝑣 ) = 𝑤 ) )
45		2fveq3	⊢ ( ( ^◡ 𝐺 ‘ 𝑣 ) = 𝑤 → ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) = ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) )
46	44 45	syl6	⊢ ( 𝑤 ∈ ω → ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) = ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) ) )
47	46	imp	⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) → ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) = ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) )
48		vex	⊢ 𝑣 ∈ V
49		vex	⊢ 𝑧 ∈ V
50	48 49	op2ndd	⊢ ( ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) = 𝑧 )
51	50	adantl	⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) → ( 2^nd ‘ ( 𝑅 ‘ 𝑤 ) ) = 𝑧 )
52	47 51	eqtr2d	⊢ ( ( 𝑤 ∈ ω ∧ ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ ) → 𝑧 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) )
53	52	rexlimiva	⊢ ( ∃ 𝑤 ∈ ω ( 𝑅 ‘ 𝑤 ) = ⟨ 𝑣 , 𝑧 ⟩ → 𝑧 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) )
54	36 53	sylbi	⊢ ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) )
55	32 54	mpg	⊢ ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 )
56	55	ax-gen	⊢ ∀ 𝑣 ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 )
57		dffun5	⊢ ( Fun 𝑆 ↔ ( Rel 𝑆 ∧ ∀ 𝑣 ∃ 𝑤 ∀ 𝑧 ( ⟨ 𝑣 , 𝑧 ⟩ ∈ 𝑆 → 𝑧 = 𝑤 ) ) )
58	27 56 57	mpbir2an	⊢ Fun 𝑆
59		dmss	⊢ ( 𝑆 ⊆ ( ( ℤ_≥ ‘ 𝐶 ) × V ) → dom 𝑆 ⊆ dom ( ( ℤ_≥ ‘ 𝐶 ) × V ) )
60	23 59	ax-mp	⊢ dom 𝑆 ⊆ dom ( ( ℤ_≥ ‘ 𝐶 ) × V )
61		dmxpss	⊢ dom ( ( ℤ_≥ ‘ 𝐶 ) × V ) ⊆ ( ℤ_≥ ‘ 𝐶 )
62	60 61	sstri	⊢ dom 𝑆 ⊆ ( ℤ_≥ ‘ 𝐶 )
63	1 2 3 4	uzrdglem	⊢ ( 𝑣 ∈ ( ℤ_≥ ‘ 𝐶 ) → ⟨ 𝑣 , ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ⟩ ∈ ran 𝑅 )
64	63 5	eleqtrrdi	⊢ ( 𝑣 ∈ ( ℤ_≥ ‘ 𝐶 ) → ⟨ 𝑣 , ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ⟩ ∈ 𝑆 )
65	48 28	opeldm	⊢ ( ⟨ 𝑣 , ( 2^nd ‘ ( 𝑅 ‘ ( ^◡ 𝐺 ‘ 𝑣 ) ) ) ⟩ ∈ 𝑆 → 𝑣 ∈ dom 𝑆 )
66	64 65	syl	⊢ ( 𝑣 ∈ ( ℤ_≥ ‘ 𝐶 ) → 𝑣 ∈ dom 𝑆 )
67	66	ssriv	⊢ ( ℤ_≥ ‘ 𝐶 ) ⊆ dom 𝑆
68	62 67	eqssi	⊢ dom 𝑆 = ( ℤ_≥ ‘ 𝐶 )
69		df-fn	⊢ ( 𝑆 Fn ( ℤ_≥ ‘ 𝐶 ) ↔ ( Fun 𝑆 ∧ dom 𝑆 = ( ℤ_≥ ‘ 𝐶 ) ) )
70	58 68 69	mpbir2an	⊢ 𝑆 Fn ( ℤ_≥ ‘ 𝐶 )

Metamath Proof Explorer

Theorem uzrdgfni

Proof