Theorem f1we

Description: Pull back a well ordering by a one-to-one function. (Contributed by Eric Schmidt, 4-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		f1owe.1	$$⊢R=\left\{⟨x,y⟩|F\left(x\right)SF\left(y\right)\right\}$$
2		f1f	$$⊢F:A\underset{1-1}{⟶}B\to F:A⟶B$$
3		frn	$$⊢F:A⟶B\to \mathrm{ran}F\subseteq B$$
4		wess	$$⊢\mathrm{ran}F\subseteq B\to \left(S\mathrm{We}B\to S\mathrm{We}\mathrm{ran}F\right)$$
5	2 3 4	3syl	$$⊢F:A\underset{1-1}{⟶}B\to \left(S\mathrm{We}B\to S\mathrm{We}\mathrm{ran}F\right)$$
6		f1f1orn	$$⊢F:A\underset{1-1}{⟶}B\to F:A\underset{1-1\; onto}{⟶}\mathrm{ran}F$$
7	1	f1owe	$$⊢F:A\underset{1-1\; onto}{⟶}\mathrm{ran}F\to \left(R\mathrm{We}A\leftrightarrow S\mathrm{We}\mathrm{ran}F\right)$$
8	6 7	syl	$$⊢F:A\underset{1-1}{⟶}B\to \left(R\mathrm{We}A\leftrightarrow S\mathrm{We}\mathrm{ran}F\right)$$
9	5 8	sylibrd	$$⊢F:A\underset{1-1}{⟶}B\to \left(S\mathrm{We}B\to R\mathrm{We}A\right)$$