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	⊢ 𝐻 = ( 𝐹 ↾ 𝐴 )
Assertion	vonf1oonf1	⊢ ( 𝐹 : V –1-1-onto→ On → 𝐻 : 𝐴 –1-1→ On )

Proof

Step	Hyp	Ref	Expression
1		vonf1oonf1.1	⊢ 𝐻 = ( 𝐹 ↾ 𝐴 )
2		f1of1	⊢ ( 𝐹 : V –1-1-onto→ On → 𝐹 : V –1-1→ On )
3		ssv	⊢ 𝐴 ⊆ V
4		f1ssres	⊢ ( ( 𝐹 : V –1-1→ On ∧ 𝐴 ⊆ V ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On )
5	2 3 4	sylancl	⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On )
6		f1eq1	⊢ ( 𝐻 = ( 𝐹 ↾ 𝐴 ) → ( 𝐻 : 𝐴 –1-1→ On ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On ) )
7	1 6	ax-mp	⊢ ( 𝐻 : 𝐴 –1-1→ On ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ On )
8	5 7	sylibr	⊢ ( 𝐹 : V –1-1-onto→ On → 𝐻 : 𝐴 –1-1→ On )