Theorem dmr0ss

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

	Ref	Expression
Assertion	dmr0ss	Could not format assertion : No typesetting found for |- dom _R0 C_ ( On X. On ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-r0	Could not format _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 ) ) ) } : No typesetting found for |- _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 ) ) ) } with typecode |-
2		simpll	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
3	2	pm4.71ri	Could not format ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) with typecode |-
4	3	opabbii	Could not format { <. 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 ) ) ) ) } : No typesetting found for |- { <. 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 ) ) ) ) } with typecode |-
5	1 4	eqtri	Could not format _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 ) ) ) ) } : No typesetting found for |- _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 ) ) ) ) } with typecode |-
6	5	dmeqi	Could not format 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 ) ) ) ) } : No typesetting found for |- 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 ) ) ) ) } with typecode |-
7		dmopabss	Could not format 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 ) : No typesetting found for |- 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 ) with typecode |-
8	6 7	eqsstri	Could not format dom _R0 C_ ( On X. On ) : No typesetting found for |- dom _R0 C_ ( On X. On ) with typecode |-