Theorem f1owe

Description: Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997) Strengthen to biconditional. (Revised by Eric Schmidt, 5-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		f1owe.1	$$⊢R=\left\{⟨x,y⟩|F\left(x\right)SF\left(y\right)\right\}$$
2		fveq2	$$⊢x=z\to F\left(x\right)=F\left(z\right)$$
3	2	breq1d	$$⊢x=z\to \left(F\left(x\right)SF\left(y\right)\leftrightarrow F\left(z\right)SF\left(y\right)\right)$$
4		fveq2	$$⊢y=w\to F\left(y\right)=F\left(w\right)$$
5	4	breq2d	$$⊢y=w\to \left(F\left(z\right)SF\left(y\right)\leftrightarrow F\left(z\right)SF\left(w\right)\right)$$
6	3 5 1	brabg	$$⊢\left(z\in A\wedge w\in A\right)\to \left(zRw\leftrightarrow F\left(z\right)SF\left(w\right)\right)$$
7	6	rgen2	$$⊢\forall z\in A\forall w\in A\left(zRw\leftrightarrow F\left(z\right)SF\left(w\right)\right)$$
8		df-isom	$$⊢F{Isom}_{R,S}\left(A,B\right)\leftrightarrow \left(F:A\underset{1-1\; onto}{⟶}B\wedge \forall z\in A\forall w\in A\left(zRw\leftrightarrow F\left(z\right)SF\left(w\right)\right)\right)$$
9		isowe	$$⊢F{Isom}_{R,S}\left(A,B\right)\to \left(R\mathrm{We}A\leftrightarrow S\mathrm{We}B\right)$$
10	8 9	sylbir	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge \forall z\in A\forall w\in A\left(zRw\leftrightarrow F\left(z\right)SF\left(w\right)\right)\right)\to \left(R\mathrm{We}A\leftrightarrow S\mathrm{We}B\right)$$
11	7 10	mpan2	$$⊢F:A\underset{1-1\; onto}{⟶}B\to \left(R\mathrm{We}A\leftrightarrow S\mathrm{We}B\right)$$