Theorem vonf1osev

Description: If F is a bijection from the universe to the ordinals, then R is a set-like well-ordering of the universe. This is the ZFC version of (2 -> 4) which is used in place of (3 -> 4) in https://tinyurl.com/hamkins-gblac . This proof takes advantage of the fact that the well-order constructed in (2 -> 3) is also set-like. (Contributed by BTernaryTau, 8-Jun-2026)

	Ref	Expression
Hypothesis	vonf1osev.1	|- R = { <. x , y >. | ( F ` x ) e. ( F ` y ) }
Assertion	vonf1osev	|- ( F : _V -1-1-onto-> On -> ( R We _V /\ R Se _V ) )

Proof

Step	Hyp	Ref	Expression
1		vonf1osev.1	|- R = { <. x , y >. | ( F ` x ) e. ( F ` y ) }
2	1	vonf1owev	|- ( F : _V -1-1-onto-> On -> R We _V )
3		vex	|- w e. _V
4		vex	|- z e. _V
5		fveq2	|- ( x = w -> ( F ` x ) = ( F ` w ) )
6	5	eleq1d	|- ( x = w -> ( ( F ` x ) e. ( F ` y ) <-> ( F ` w ) e. ( F ` y ) ) )
7		fveq2	|- ( y = z -> ( F ` y ) = ( F ` z ) )
8	7	eleq2d	|- ( y = z -> ( ( F ` w ) e. ( F ` y ) <-> ( F ` w ) e. ( F ` z ) ) )
9	3 4 6 8 1	brab	|- ( w R z <-> ( F ` w ) e. ( F ` z ) )
10		fvex	|- ( F ` z ) e. _V
11	10	epeli	|- ( ( F ` w ) _E ( F ` z ) <-> ( F ` w ) e. ( F ` z ) )
12	9 11	bitr4i	|- ( w R z <-> ( F ` w ) _E ( F ` z ) )
13	12	rgen2w	|- A. w e. _V A. z e. _V ( w R z <-> ( F ` w ) _E ( F ` z ) )
14		df-isom	|- ( F Isom R , _E ( _V , On ) <-> ( F : _V -1-1-onto-> On /\ A. w e. _V A. z e. _V ( w R z <-> ( F ` w ) _E ( F ` z ) ) ) )
15	13 14	mpbiran2	|- ( F Isom R , _E ( _V , On ) <-> F : _V -1-1-onto-> On )
16		epse	|- _E Se On
17		isose	|- ( F Isom R , _E ( _V , On ) -> ( R Se _V <-> _E Se On ) )
18	16 17	mpbiri	|- ( F Isom R , _E ( _V , On ) -> R Se _V )
19	15 18	sylbir	|- ( F : _V -1-1-onto-> On -> R Se _V )
20	2 19	jca	|- ( F : _V -1-1-onto-> On -> ( R We _V /\ R Se _V ) )