もう一段階さかのぼったほうがいいかな。
g:Y→Xが写像であるということを明確に定義できる？

fが全射であること、単射であることを論理的に定義し、
そこから論理的推論で写像gが曖昧な部分を残さずに定義されることを書かなきゃ納得できない。