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	⊢ ( 𝐹 : 𝐴 –1-1→ On → ( 𝐹 : 𝐴 –1-1→ On ∨ 𝐻 : On –1-1→ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		orc	⊢ ( 𝐹 : 𝐴 –1-1→ On → ( 𝐹 : 𝐴 –1-1→ On ∨ 𝐻 : On –1-1→ 𝐴 ) )