Theorem wevsev

Description: If R is a well-ordering of the universe, then S is a set-like well-ordering of the universe. This is the ZFC version of (3 -> 4) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 18-Sep-2026)

	Ref	Expression
Hypothesis	wevsev.1	|- S = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) }
Assertion	wevsev	|- ( R We _V -> ( S We _V /\ S Se _V ) )

Proof

Step	Hyp	Ref	Expression
1		wevsev.1	|- S = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) }
2		ssv	|- { z e. _V | ( rank ` z ) = ( rank ` w ) } C_ _V
3		wess	|- ( { z e. _V | ( rank ` z ) = ( rank ` w ) } C_ _V -> ( R We _V -> R We { z e. _V | ( rank ` z ) = ( rank ` w ) } ) )
4	2 3	ax-mp	|- ( R We _V -> R We { z e. _V | ( rank ` z ) = ( rank ` w ) } )
5	4	ralrimivw	|- ( R We _V -> A. w e. _V R We { z e. _V | ( rank ` z ) = ( rank ` w ) } )
6	1	werankwe2	|- ( A. w e. _V R We { z e. _V | ( rank ` z ) = ( rank ` w ) } -> S We _V )
7	5 6	syl	|- ( R We _V -> S We _V )
8	1	rankse	|- S Se _V
9	7 8	jctir	|- ( R We _V -> ( S We _V /\ S Se _V ) )