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\underset{1-1}{⟶}\mathrm{On}\to \left(F:A\underset{1-1}{⟶}\mathrm{On}\vee H:\mathrm{On}\underset{1-1}{⟶}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		orc	$$⊢F:A\underset{1-1}{⟶}\mathrm{On}\to \left(F:A\underset{1-1}{⟶}\mathrm{On}\vee H:\mathrm{On}\underset{1-1}{⟶}A\right)$$