Metamath Proof Explorer

Theorem dmr0ss

Description: The domain of _R0 is a subset of On X. On . (Contributed by BTernaryTau, 22-Sep-2026)

		Ref	Expression
	Assertion	dmr0ss	⊢ dom 𝑅₀ ⊆ ( On × On )

Proof

Step	Hyp	Ref	Expression
1		df-r0	⊢ 𝑅₀ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) }
2		simpll	⊢ ( ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) → 𝑥 ∈ ( On × On ) )
3	2	pm4.71ri	⊢ ( ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) ↔ ( 𝑥 ∈ ( On × On ) ∧ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) ) )
4	3	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) ) }
5	1 4	eqtri	⊢ 𝑅₀ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) ) }
6	5	dmeqi	⊢ dom 𝑅₀ = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) ) }
7		dmopabss	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∨ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 LexOrd 𝑦 ) ) ) ) } ⊆ ( On × On )
8	6 7	eqsstri	⊢ dom 𝑅₀ ⊆ ( On × On )