Metamath Proof Explorer

Definition df-r0

Description: Define a particular set-like well-ordering of On X. On using the lexicographical ordering LexOrd . Based on Definition 7.57 of TakeutiZaring p. 54. (Contributed by BTernaryTau, 2-Sep-2026)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cr0 
 |-  _R0
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 con0 
 |-  On
5 4 4 cxp 
 |-  ( On X. On )
6 3 5 wcel 
 |-  x e. ( On X. On )
7 2 cv 
 |-  y
8 7 5 wcel 
 |-  y e. ( On X. On )
9 6 8 wa 
 |-  ( x e. ( On X. On ) /\ y e. ( On X. On ) )
10 c1st 
 |-  1st
11 3 10 cfv 
 |-  ( 1st ` x )
12 c2nd 
 |-  2nd
13 3 12 cfv 
 |-  ( 2nd ` x )
14 11 13 cun 
 |-  ( ( 1st ` x ) u. ( 2nd ` x ) )
15 7 10 cfv 
 |-  ( 1st ` y )
16 7 12 cfv 
 |-  ( 2nd ` y )
17 15 16 cun 
 |-  ( ( 1st ` y ) u. ( 2nd ` y ) )
18 14 17 wcel 
 |-  ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) )
19 14 17 wceq 
 |-  ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) )
20 clexo 
 |-  LexOrd
21 3 7 20 wbr 
 |-  x LexOrd y
22 19 21 wa 
 |-  ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y )
23 18 22 wo 
 |-  ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) )
24 9 23 wa 
 |-  ( ( 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 ) ) )
25 24 1 2 copab 
 |-  { <. 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 ) ) ) }
26 0 25 wceq 
 |-  _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 ) ) ) }