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 |` A )
Assertion	vonf1oonf1	|- ( F : _V -1-1-onto-> On -> H : A -1-1-> On )

Proof

Step	Hyp	Ref	Expression
1		vonf1oonf1.1	|- H = ( F |` A )
2		f1of1	|- ( F : _V -1-1-onto-> On -> F : _V -1-1-> On )
3		ssv	|- A C_ _V
4		f1ssres	|- ( ( F : _V -1-1-> On /\ A C_ _V ) -> ( F |` A ) : A -1-1-> On )
5	2 3 4	sylancl	|- ( F : _V -1-1-onto-> On -> ( F |` A ) : A -1-1-> On )
6		f1eq1	|- ( H = ( F |` A ) -> ( H : A -1-1-> On <-> ( F |` A ) : A -1-1-> On ) )
7	1 6	ax-mp	|- ( H : A -1-1-> On <-> ( F |` A ) : A -1-1-> On )
8	5 7	sylibr	|- ( F : _V -1-1-onto-> On -> H : A -1-1-> On )