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	Could not format assertion : 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 |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cr0	Could not format _R0 : No typesetting found for class _R0 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		c2nd	$$class{2}^{nd}$$
13	3 12	cfv	$$class{2}^{nd}\left(x\right)$$
14	11 13	cun	$$class\left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)$$
15	7 10	cfv	$$class{1}^{st}\left(y\right)$$
16	7 12	cfv	$$class{2}^{nd}\left(y\right)$$
17	15 16	cun	$$class\left(1^{st}\left(y\right)\cup 2^{nd}\left(y\right)\right)$$
18	14 17	wcel	$$wff{1}^{st}\left(x\right)\cup 2^{nd}\left(x\right)\in \left(1^{st}\left(y\right)\cup 2^{nd}\left(y\right)\right)$$
19	14 17	wceq	$$wff{1}^{st}\left(x\right)\cup 2^{nd}\left(x\right)=1^{st}\left(y\right)\cup 2^{nd}\left(y\right)$$
20		clexo	Could not format LexOrd : No typesetting found for class LexOrd with typecode class
21	3 7 20	wbr	Could not format x LexOrd y : No typesetting found for wff x LexOrd y with typecode wff
22	19 21	wa	Could not format ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) : No typesetting found for wff ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) with typecode wff
23	18 22	wo	Could not format ( ( ( 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 wff ( ( ( 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 wff
24	9 23	wa	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 ) ) ) : No typesetting found for wff ( ( 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 wff
25	24 1 2	copab	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 ) ) ) } : No typesetting found for class { <. 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 class
26	0 25	wceq	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 wff _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 wff