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

Proof

Step	Hyp	Ref	Expression
1		onf1we.1	|- R = { <. x , y >. | ( F ` x ) e. ( F ` y ) }
2		f1f	|- ( F : A -1-1-> On -> F : A --> On )
3	2	frnd	|- ( F : A -1-1-> On -> ran F C_ On )
4		epweon	|- _E We On
5		wess	|- ( ran F C_ On -> ( _E We On -> _E We ran F ) )
6	3 4 5	mpisyl	|- ( F : A -1-1-> On -> _E We ran F )
7		f1f1orn	|- ( F : A -1-1-> On -> F : A -1-1-onto-> ran F )
8		fvex	|- ( F ` y ) e. _V
9	8	epeli	|- ( ( F ` x ) _E ( F ` y ) <-> ( F ` x ) e. ( F ` y ) )
10	9	opabbii	|- { <. x , y >. | ( F ` x ) _E ( F ` y ) } = { <. x , y >. | ( F ` x ) e. ( F ` y ) }
11	1 10	eqtr4i	|- R = { <. x , y >. | ( F ` x ) _E ( F ` y ) }
12	11	f1owe	|- ( F : A -1-1-onto-> ran F -> ( R We A <-> _E We ran F ) )
13	7 12	syl	|- ( F : A -1-1-> On -> ( R We A <-> _E We ran F ) )
14	6 13	mpbird	|- ( F : A -1-1-> On -> R We A )