Metamath Proof Explorer

Theorem brr0d

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

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

Proof

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