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	Could not format assertion : No typesetting found for |- 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 ) ) ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clexo	Could not format LexOrd : No typesetting found for class LexOrd with typecode class
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4		con0	$$class\mathrm{On}$$
5	4 4	cxp	$$class\left(\mathrm{On}\times \mathrm{On}\right)$$
6	3 5	wcel	$$wffx\in \left(\mathrm{On}\times \mathrm{On}\right)$$
7	2	cv	$$setvary$$
8	7 5	wcel	$$wffy\in \left(\mathrm{On}\times \mathrm{On}\right)$$
9	6 8	wa	$$wff\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)$$
10		c1st	$$class{1}^{st}$$
11	3 10	cfv	$$class{1}^{st}\left(x\right)$$
12	7 10	cfv	$$class{1}^{st}\left(y\right)$$
13	11 12	wcel	$$wff{1}^{st}\left(x\right)\in 1^{st}\left(y\right)$$
14	11 12	wceq	$$wff{1}^{st}\left(x\right)=1^{st}\left(y\right)$$
15		c2nd	$$class{2}^{nd}$$
16	3 15	cfv	$$class{2}^{nd}\left(x\right)$$
17	7 15	cfv	$$class{2}^{nd}\left(y\right)$$
18	16 17	wcel	$$wff{2}^{nd}\left(x\right)\in 2^{nd}\left(y\right)$$
19	14 18	wa	$$wff\left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)$$
20	13 19	wo	$$wff\left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)$$
21	9 20	wa	$$wff\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)$$
22	21 1 2	copab	$$class\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)\right\}$$
23	0 22	wceq	Could not format 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 ) ) ) ) } : No typesetting found for wff 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 ) ) ) ) } with typecode wff