This formula is upward absolute between transitive models: if the smaller model contains such an f, the assumed absoluteness of “function”, domain, range, and ω shows that the same witness works in the larger model.
The generic union g=⋃G is a total map ω→α, because the conditions deciding each input form adense set. For every β<α, the conditions putting β somewhere in the range are also dense, so g is surjective. Thus M[G]⊨φ1(α). But M⊨φ1(α) because M regards αas its first uncountable ordinal. Hence φ1 is not downward absolute between M and M[G].