Theorem vonf1oonf1

Description: If F is a bijection from the universe to the ordinals, then H maps A one-to-one into the ordinals. This is the ZFC version of (5 -> 6) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the antecedent would be something like A. X ( -. X e.V -> E. F F : X -1-1-onto-> On ) , but since we cannot quantify over classes, we instead consider only the case X = V which is sufficient for this proof. This theorem can also be viewed as (2 -> 6). (Contributed by BTernaryTau, 10-Jun-2026)

	Ref	Expression
Hypothesis	vonf1oonf1.1	$$⊢H={F\upharpoonright }_A$$
Assertion	vonf1oonf1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to H:A\underset{1-1}{⟶}\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		vonf1oonf1.1	$$⊢H={F\upharpoonright }_A$$
2		f1of1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to F:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}$$
3		ssv	$$⊢A\subseteq \mathrm{V}$$
4		f1ssres	$$⊢\left(F:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}\wedge A\subseteq \mathrm{V}\right)\to \left({F\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}$$
5	2 3 4	sylancl	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to \left({F\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}$$
6		f1eq1	$$⊢H={F\upharpoonright }_A\to \left(H:A\underset{1-1}{⟶}\mathrm{On}\leftrightarrow \left({F\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}\right)$$
7	1 6	ax-mp	$$⊢H:A\underset{1-1}{⟶}\mathrm{On}\leftrightarrow \left({F\upharpoonright }_A\right):A\underset{1-1}{⟶}\mathrm{On}$$
8	5 7	sylibr	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to H:A\underset{1-1}{⟶}\mathrm{On}$$