Description: If F maps A one-to-one into the ordinals or H maps the
ordinals one-to-one into A , then either A can be mapped
one-to-one into the ordinals (by F ), or the ordinals can be mapped
one-to-one into A (by H ). This is the ZFC version of (10 ->
9) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory
the antecedent would be something like
A. A A. X ( E. F F : A -1-1-> X \/ E. H H : X -1-1-> A ) , but since
we cannot quantify over classes, we instead consider only the case
X = On which is sufficient for this proof. The proof is trivial but
is included for completeness. (Contributed by BTernaryTau, 17-Sep-2026)