Theorem f1oronf1or 36056

Description: If 𝐹 maps 𝐴 one-to-one into the ordinals or 𝐻 maps the ordinals one-to-one into 𝐴, then either 𝐴 can be mapped one-to-one into the ordinals (by 𝐹), or the ordinals can be mapped one-to-one into 𝐴 (by 𝐻). 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 ∀𝐴∀𝑋(∃𝐹𝐹:𝐴⟶1-1𝑋 ∨ ∃𝐻𝐻:𝑋⟶1-1𝐴), but since we cannot quantify over classes, we instead consider only the case 𝑋 = On which is sufficient for this proof. The proof is trivial but is included for completeness. (Contributed by BTernaryTau, 17-Sep-2026.)

Assertion

Ref	Expression
f1oronf1or	⊢ ((𝐹:𝐴⟶1-1On ∨ 𝐻:On⟶1-1𝐴) → (𝐹:𝐴⟶1-1On ∨ 𝐻:On⟶1-1𝐴))

Proof of Theorem f1oronf1or

Step	Hyp	Ref	Expression
1		id 23	1 ⊢ ((𝐹:𝐴⟶1-1On ∨ 𝐻:On⟶1-1𝐴) → (𝐹:𝐴⟶1-1On ∨ 𝐻:On⟶1-1𝐴))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861  Oncon0 6380  ⟶1-1wf1 6555

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by: (None)