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 = { <. x , y >. | ( F ` x ) S ( F ` y ) }
Assertion	f1we	|- ( F : A -1-1-> B -> ( S We B -> R We A ) )

Proof

Step	Hyp	Ref	Expression
1		f1owe.1	|- R = { <. x , y >. | ( F ` x ) S ( F ` y ) }
2		f1f	|- ( F : A -1-1-> B -> F : A --> B )
3		frn	|- ( F : A --> B -> ran F C_ B )
4		wess	|- ( ran F C_ B -> ( S We B -> S We ran F ) )
5	2 3 4	3syl	|- ( F : A -1-1-> B -> ( S We B -> S We ran F ) )
6		f1f1orn	|- ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
7	1	f1owe	|- ( F : A -1-1-onto-> ran F -> ( R We A <-> S We ran F ) )
8	6 7	syl	|- ( F : A -1-1-> B -> ( R We A <-> S We ran F ) )
9	5 8	sylibrd	|- ( F : A -1-1-> B -> ( S We B -> R We A ) )