Theorem om2noseqfo

Description: Function statement for G . (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 ) ) , 𝐶 ) “ ω ) )
Assertion	om2noseqfo	⊢ ( 𝜑 → 𝐺 : ω –onto→ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
2		om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3		om2noseq.3	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4		frfnom	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) Fn ω
5	2	fneq1d	⊢ ( 𝜑 → ( 𝐺 Fn ω ↔ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) Fn ω ) )
6	4 5	mpbiri	⊢ ( 𝜑 → 𝐺 Fn ω )
7		df-ima	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω )
8	7	eqcomi	⊢ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω )
9	2	rneqd	⊢ ( 𝜑 → ran 𝐺 = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
10	8 9 3	3eqtr4a	⊢ ( 𝜑 → ran 𝐺 = 𝑍 )
11		df-fo	⊢ ( 𝐺 : ω –onto→ 𝑍 ↔ ( 𝐺 Fn ω ∧ ran 𝐺 = 𝑍 ) )
12	6 10 11	sylanbrc	⊢ ( 𝜑 → 𝐺 : ω –onto→ 𝑍 )