Theorem f1oronf1or

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)

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

Proof

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