om2noseqfo

Description: Function statement for G . (Contributed by Scott Fenton, 18-Apr-2025)

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		frfnom	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) Fn ω$
5	2	fneq1d	$⊢ φ \to (G Fn ω \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) Fn ω)$
6	4 5	mpbiri	$⊢ φ \to G Fn ω$
7		df-ima	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω] = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω})$
8	7	eqcomi	$⊢ ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) = rec ((x \in V ⟼ x +_{s} 1_{s}), C) [ω]$
9	2	rneqd	$⊢ φ \to ran G = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω})$
10	8 9 3	3eqtr4a	$⊢ φ \to ran G = Z$
11		df-fo	$⊢ G : ω \underset{onto}{⟶} Z \leftrightarrow (G Fn ω \land ran G = Z)$
12	6 10 11	sylanbrc	$⊢ φ \to G : ω \underset{onto}{⟶} Z$

Metamath Proof Explorer