Metamath Proof Explorer

Theorem brlexod

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

Ref Expression
Hypotheses brlexod.1 
|- ( ph -> A e. On )
brlexod.2 
|- ( ph -> B e. On )
brlexod.3 
|- ( ph -> C e. On )
brlexod.4 
|- ( ph -> D e. On )
Assertion brlexod 
|- ( ph -> ( <. A , B >. LexOrd <. C , D >. <-> ( A e. C \/ ( A = C /\ B e. D ) ) ) )

Proof

Step Hyp Ref Expression
1 brlexod.1 
 |-  ( ph -> A e. On )
2 brlexod.2 
 |-  ( ph -> B e. On )
3 brlexod.3 
 |-  ( ph -> C e. On )
4 brlexod.4 
 |-  ( ph -> D e. On )
5 1 2 opelxpd 
 |-  ( ph -> <. A , B >. e. ( On X. On ) )
6 3 4 opelxpd 
 |-  ( ph -> <. C , D >. e. ( On X. On ) )
7 5 6 jca 
 |-  ( ph -> ( <. A , B >. e. ( On X. On ) /\ <. C , D >. e. ( On X. On ) ) )
8 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 ) ) ) ) }
9 8 a1i 
 |-  ( 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 ) ) ) ) } )
10 fveq2 
 |-  ( x = <. A , B >. -> ( 1st ` x ) = ( 1st ` <. A , B >. ) )
11 op1stg 
 |-  ( ( A e. On /\ B e. On ) -> ( 1st ` <. A , B >. ) = A )
12 1 2 11 syl2anc 
 |-  ( ph -> ( 1st ` <. A , B >. ) = A )
13 10 12 sylan9eqr 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 1st ` x ) = A )
14 13 adantrr 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( 1st ` x ) = A )
15 fveq2 
 |-  ( y = <. C , D >. -> ( 1st ` y ) = ( 1st ` <. C , D >. ) )
16 op1stg 
 |-  ( ( C e. On /\ D e. On ) -> ( 1st ` <. C , D >. ) = C )
17 3 4 16 syl2anc 
 |-  ( ph -> ( 1st ` <. C , D >. ) = C )
18 15 17 sylan9eqr 
 |-  ( ( ph /\ y = <. C , D >. ) -> ( 1st ` y ) = C )
19 18 adantrl 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( 1st ` y ) = C )
20 14 19 eleq12d 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( 1st ` x ) e. ( 1st ` y ) <-> A e. C ) )
21 14 19 eqeq12d 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( 1st ` x ) = ( 1st ` y ) <-> A = C ) )
22 fveq2 
 |-  ( x = <. A , B >. -> ( 2nd ` x ) = ( 2nd ` <. A , B >. ) )
23 op2ndg 
 |-  ( ( A e. On /\ B e. On ) -> ( 2nd ` <. A , B >. ) = B )
24 1 2 23 syl2anc 
 |-  ( ph -> ( 2nd ` <. A , B >. ) = B )
25 22 24 sylan9eqr 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 2nd ` x ) = B )
26 25 adantrr 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( 2nd ` x ) = B )
27 fveq2 
 |-  ( y = <. C , D >. -> ( 2nd ` y ) = ( 2nd ` <. C , D >. ) )
28 op2ndg 
 |-  ( ( C e. On /\ D e. On ) -> ( 2nd ` <. C , D >. ) = D )
29 3 4 28 syl2anc 
 |-  ( ph -> ( 2nd ` <. C , D >. ) = D )
30 27 29 sylan9eqr 
 |-  ( ( ph /\ y = <. C , D >. ) -> ( 2nd ` y ) = D )
31 30 adantrl 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( 2nd ` y ) = D )
32 26 31 eleq12d 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( 2nd ` x ) e. ( 2nd ` y ) <-> B e. D ) )
33 21 32 anbi12d 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) <-> ( A = C /\ B e. D ) ) )
34 20 33 orbi12d 
 |-  ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) <-> ( A e. C \/ ( A = C /\ B e. D ) ) ) )
35 9 34 brab2d 
 |-  ( 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 ) ) ) ) )
36 7 35 mpbirand 
 |-  ( ph -> ( <. A , B >. LexOrd <. C , D >. <-> ( A e. C \/ ( A = C /\ B e. D ) ) ) )