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	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) }
Assertion	wevsev	⊢ ( 𝑅 We V → ( 𝑆 We V ∧ 𝑆 Se V ) )

Proof

Step	Hyp	Ref	Expression
1		wevsev.1	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) }
2		ssv	⊢ { 𝑧 ∈ V ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑤 ) } ⊆ V
3		wess	⊢ ( { 𝑧 ∈ V ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑤 ) } ⊆ V → ( 𝑅 We V → 𝑅 We { 𝑧 ∈ V ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑤 ) } ) )
4	2 3	ax-mp	⊢ ( 𝑅 We V → 𝑅 We { 𝑧 ∈ V ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑤 ) } )
5	4	ralrimivw	⊢ ( 𝑅 We V → ∀ 𝑤 ∈ V 𝑅 We { 𝑧 ∈ V ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑤 ) } )
6	1	werankwe2	⊢ ( ∀ 𝑤 ∈ V 𝑅 We { 𝑧 ∈ V ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑤 ) } → 𝑆 We V )
7	5 6	syl	⊢ ( 𝑅 We V → 𝑆 We V )
8	1	rankse	⊢ 𝑆 Se V
9	7 8	jctir	⊢ ( 𝑅 We V → ( 𝑆 We V ∧ 𝑆 Se V ) )