Theorem vonf1owev

Description: If F is a bijection from the universe to the ordinals, then R well-orders the universe. This is the ZFC version of (2 -> 3) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 6-Dec-2025) (Proof shortened by BTernaryTau, 11-Jun-2026)

	Ref	Expression
Hypothesis	vonf1owev.1	$$⊢R=\left\{⟨x,y⟩|F\left(x\right)\in F\left(y\right)\right\}$$
Assertion	vonf1owev	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to R\mathrm{We}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vonf1owev.1	$$⊢R=\left\{⟨x,y⟩|F\left(x\right)\in F\left(y\right)\right\}$$
2		f1of1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to F:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}$$
3	1	vonf1wev	$$⊢F:\mathrm{V}\underset{1-1}{⟶}\mathrm{On}\to R\mathrm{We}\mathrm{V}$$
4	2 3	syl	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{On}\to R\mathrm{We}\mathrm{V}$$