Metamath Proof Explorer

Definition df-lexo

Description: Define the lexicographical ordering of On X. On . Based on Definition 7.55 of TakeutiZaring p. 54. (Contributed by BTernaryTau, 2-Sep-2026)

Ref Expression
Assertion df-lexo 
|- LexOrd = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clexo 
 |-  LexOrd
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 7 10 cfv 
 |-  ( 1st ` y )
13 11 12 wcel 
 |-  ( 1st ` x ) e. ( 1st ` y )
14 11 12 wceq 
 |-  ( 1st ` x ) = ( 1st ` y )
15 c2nd 
 |-  2nd
16 3 15 cfv 
 |-  ( 2nd ` x )
17 7 15 cfv 
 |-  ( 2nd ` y )
18 16 17 wcel 
 |-  ( 2nd ` x ) e. ( 2nd ` y )
19 14 18 wa 
 |-  ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) )
20 13 19 wo 
 |-  ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) )
21 9 20 wa 
 |-  ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) )
22 21 1 2 copab 
 |-  { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
23 0 22 wceq 
 |-  LexOrd = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }