[red75prime]

It seems to be even easier: BB codomain is a set of standard natural numbers regardless of which model of ZFS we are using. Therefore BB(748)=Q is false for every non-standard natural number Q.

We can come up with some function BB' that admits that, but it's just a different function.

It seems we can't even define a function with standard domain and non-standard codomain while not using literals for non-standard numbers in its definition.

That is ~(BB(748)=ActualValueOfBB748) is false even if it can't be proven in ZFC. In a sense, busy beaver creates its own mathematical reality.