Theorem brlexod

Description: Condition for two ordered pairs to be related by LexOrd . (Contributed by BTernaryTau, 20-Sep-2026)

	Ref	Expression
Hypotheses	brlexod.1	$$⊢\phi \to A\in \mathrm{On}$$
	brlexod.2	$$⊢\phi \to B\in \mathrm{On}$$
	brlexod.3	$$⊢\phi \to C\in \mathrm{On}$$
	brlexod.4	$$⊢\phi \to D\in \mathrm{On}$$
Assertion	brlexod	Could not format assertion : No typesetting found for |- ( ph -> ( <. A , B >. LexOrd <. C , D >. <-> ( A e. C \/ ( A = C /\ B e. D ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		brlexod.1	$$⊢\phi \to A\in \mathrm{On}$$
2		brlexod.2	$$⊢\phi \to B\in \mathrm{On}$$
3		brlexod.3	$$⊢\phi \to C\in \mathrm{On}$$
4		brlexod.4	$$⊢\phi \to D\in \mathrm{On}$$
5	1 2	opelxpd	$$⊢\phi \to ⟨A,B⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
6	3 4	opelxpd	$$⊢\phi \to ⟨C,D⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
7	5 6	jca	$$⊢\phi \to \left(⟨A,B⟩\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge ⟨C,D⟩\in \left(\mathrm{On}\times \mathrm{On}\right)\right)$$
8		df-lexo	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 |- 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 |-
9	8	a1i	Could not format ( ph -> 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 |- ( ph -> 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 |-
10		fveq2	$$⊢x=⟨A,B⟩\to 1^{st}\left(x\right)=1^{st}\left(⟨A,B⟩\right)$$
11		op1stg	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$
12	1 2 11	syl2anc	$$⊢\phi \to 1^{st}\left(⟨A,B⟩\right)=A$$
13	10 12	sylan9eqr	$$⊢\left(\phi \wedge x=⟨A,B⟩\right)\to 1^{st}\left(x\right)=A$$
14	13	adantrr	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to 1^{st}\left(x\right)=A$$
15		fveq2	$$⊢y=⟨C,D⟩\to 1^{st}\left(y\right)=1^{st}\left(⟨C,D⟩\right)$$
16		op1stg	$$⊢\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\to 1^{st}\left(⟨C,D⟩\right)=C$$
17	3 4 16	syl2anc	$$⊢\phi \to 1^{st}\left(⟨C,D⟩\right)=C$$
18	15 17	sylan9eqr	$$⊢\left(\phi \wedge y=⟨C,D⟩\right)\to 1^{st}\left(y\right)=C$$
19	18	adantrl	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to 1^{st}\left(y\right)=C$$
20	14 19	eleq12d	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\leftrightarrow A\in C\right)$$
21	14 19	eqeq12d	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to \left(1^{st}\left(x\right)=1^{st}\left(y\right)\leftrightarrow A=C\right)$$
22		fveq2	$$⊢x=⟨A,B⟩\to 2^{nd}\left(x\right)=2^{nd}\left(⟨A,B⟩\right)$$
23		op2ndg	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
24	1 2 23	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨A,B⟩\right)=B$$
25	22 24	sylan9eqr	$$⊢\left(\phi \wedge x=⟨A,B⟩\right)\to 2^{nd}\left(x\right)=B$$
26	25	adantrr	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to 2^{nd}\left(x\right)=B$$
27		fveq2	$$⊢y=⟨C,D⟩\to 2^{nd}\left(y\right)=2^{nd}\left(⟨C,D⟩\right)$$
28		op2ndg	$$⊢\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\to 2^{nd}\left(⟨C,D⟩\right)=D$$
29	3 4 28	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨C,D⟩\right)=D$$
30	27 29	sylan9eqr	$$⊢\left(\phi \wedge y=⟨C,D⟩\right)\to 2^{nd}\left(y\right)=D$$
31	30	adantrl	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to 2^{nd}\left(y\right)=D$$
32	26 31	eleq12d	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to \left(2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\leftrightarrow B\in D\right)$$
33	21 32	anbi12d	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to \left(\left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\leftrightarrow \left(A=C\wedge B\in D\right)\right)$$
34	20 33	orbi12d	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to \left(\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)\leftrightarrow \left(A\in C\vee \left(A=C\wedge B\in D\right)\right)\right)$$
35	9 34	brab2d	Could not format ( ph -> ( <. A , B >. LexOrd <. C , D >. <-> ( ( <. A , B >. e. ( On X. On ) /\ <. C , D >. e. ( On X. On ) ) /\ ( A e. C \/ ( A = C /\ B e. D ) ) ) ) ) : No typesetting found for |- ( ph -> ( <. A , B >. LexOrd <. C , D >. <-> ( ( <. A , B >. e. ( On X. On ) /\ <. C , D >. e. ( On X. On ) ) /\ ( A e. C \/ ( A = C /\ B e. D ) ) ) ) ) with typecode |-
36	7 35	mpbirand	Could not format ( ph -> ( <. A , B >. LexOrd <. C , D >. <-> ( A e. C \/ ( A = C /\ B e. D ) ) ) ) : No typesetting found for |- ( ph -> ( <. A , B >. LexOrd <. C , D >. <-> ( A e. C \/ ( A = C /\ B e. D ) ) ) ) with typecode |-