Theorem onf1onf1or

Description: If F maps A one-to-one into the ordinals, 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 . This is the ZFC version of (6 -> 9) in https://tinyurl.com/hamkins-gblac . The proof is trivial but is included for completeness. (Contributed by BTernaryTau, 16-Sep-2026)

	Ref	Expression
Assertion	onf1onf1or	|- ( F : A -1-1-> On -> ( F : A -1-1-> On \/ H : On -1-1-> A ) )

Proof

Step	Hyp	Ref	Expression
1		orc	|- ( F : A -1-1-> On -> ( F : A -1-1-> On \/ H : On -1-1-> A ) )