Theorem r0weseon

Description: _R0 is a set-like well-ordering of On X. On . Part of Proposition 7.58 of TakeutiZaring p. 54. This theorem is r0weon expressed using _R0 . (Contributed by BTernaryTau, 19-Sep-2026)

	Ref	Expression
Assertion	r0weseon	⊢ ( 𝑅0 We ( On × On ) ∧ 𝑅0 Se ( On × On ) )

Proof

Step	Hyp	Ref	Expression
1		df-lexo	⊢ LexOrd = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) }
2		df-r0	⊢ 𝑅0 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) ∈ ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∨ ( ( ( 1st ‘ 𝑧 ) ∪ ( 2nd ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑤 ) ∪ ( 2nd ‘ 𝑤 ) ) ∧ 𝑧 LexOrd 𝑤 ) ) ) }
3	1 2	r0weon	⊢ ( 𝑅0 We ( On × On ) ∧ 𝑅0 Se ( On × On ) )