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 _R0 C_ ( On X. On )

Proof

Step Hyp Ref Expression
1 df-r0 
 |-  _R0 = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) }
2 simpll 
 |-  ( ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) -> x e. ( On X. On ) )
3 2 pm4.71ri 
 |-  ( ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) <-> ( x e. ( On X. On ) /\ ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) ) )
4 3 opabbii 
 |-  { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) } = { <. x , y >. | ( x e. ( On X. On ) /\ ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) ) }
5 1 4 eqtri 
 |-  _R0 = { <. x , y >. | ( x e. ( On X. On ) /\ ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) ) }
6 5 dmeqi 
 |-  dom _R0 = dom { <. x , y >. | ( x e. ( On X. On ) /\ ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) ) }
7 dmopabss 
 |-  dom { <. x , y >. | ( x e. ( On X. On ) /\ ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) ) } C_ ( On X. On )
8 6 7 eqsstri 
 |-  dom _R0 C_ ( On X. On )