Theorem onf1we

Description: If F maps A one-to-one into the ordinals, then R well-orders A . (Contributed by BTernaryTau, 16-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		onf1we.1	$$⊢R=\left\{⟨x,y⟩|F\left(x\right)\in F\left(y\right)\right\}$$
2		f1f	$$⊢F:A\underset{1-1}{⟶}\mathrm{On}\to F:A⟶\mathrm{On}$$
3	2	frnd	$$⊢F:A\underset{1-1}{⟶}\mathrm{On}\to \mathrm{ran}F\subseteq \mathrm{On}$$
4		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
5		wess	$$⊢\mathrm{ran}F\subseteq \mathrm{On}\to \left(\mathrm{E}\mathrm{We}\mathrm{On}\to \mathrm{E}\mathrm{We}\mathrm{ran}F\right)$$
6	3 4 5	mpisyl	$$⊢F:A\underset{1-1}{⟶}\mathrm{On}\to \mathrm{E}\mathrm{We}\mathrm{ran}F$$
7		f1f1orn	$$⊢F:A\underset{1-1}{⟶}\mathrm{On}\to F:A\underset{1-1\; onto}{⟶}\mathrm{ran}F$$
8		fvex	$$⊢F\left(y\right)\in \mathrm{V}$$
9	8	epeli	$$⊢F\left(x\right)\mathrm{E}F\left(y\right)\leftrightarrow F\left(x\right)\in F\left(y\right)$$
10	9	opabbii	$$⊢\left\{⟨x,y⟩|F\left(x\right)\mathrm{E}F\left(y\right)\right\}=\left\{⟨x,y⟩|F\left(x\right)\in F\left(y\right)\right\}$$
11	1 10	eqtr4i	$$⊢R=\left\{⟨x,y⟩|F\left(x\right)\mathrm{E}F\left(y\right)\right\}$$
12	11	f1owe	$$⊢F:A\underset{1-1\; onto}{⟶}\mathrm{ran}F\to \left(R\mathrm{We}A\leftrightarrow \mathrm{E}\mathrm{We}\mathrm{ran}F\right)$$
13	7 12	syl	$$⊢F:A\underset{1-1}{⟶}\mathrm{On}\to \left(R\mathrm{We}A\leftrightarrow \mathrm{E}\mathrm{We}\mathrm{ran}F\right)$$
14	6 13	mpbird	$$⊢F:A\underset{1-1}{⟶}\mathrm{On}\to R\mathrm{We}A$$