Metamath Proof Explorer

Theorem brxrn

Description: Characterize a ternary relation over a range Cartesian product. Together with xrnss3v , this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021)

Ref Expression
Assertion brxrn 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. S ) <. B , C >. <-> ( A R B /\ A S C ) ) )

Proof

Step Hyp Ref Expression
1 df-xrn 
 |-  ( R |X. S ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) )
2 1 breqi 
 |-  ( A ( R |X. S ) <. B , C >. <-> A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. )
3 2 a1i 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. S ) <. B , C >. <-> A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. ) )
4 brin 
 |-  ( A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. <-> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. /\ A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. ) )
5 4 a1i 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) <. B , C >. <-> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. /\ A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. ) ) )
6 opex 
 |-  <. B , C >. e. _V
7 brcog 
 |-  ( ( A e. V /\ <. B , C >. e. _V ) -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) ) )
8 6 7 mpan2 
 |-  ( A e. V -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) ) )
9 8 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) ) )
10 brcnvg 
 |-  ( ( x e. _V /\ <. B , C >. e. _V ) -> ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 1st |` ( _V X. _V ) ) x ) )
11 6 10 mpan2 
 |-  ( x e. _V -> ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 1st |` ( _V X. _V ) ) x ) )
12 11 elv 
 |-  ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 1st |` ( _V X. _V ) ) x )
13 opelvvg 
 |-  ( ( B e. W /\ C e. X ) -> <. B , C >. e. ( _V X. _V ) )
14 13 biantrurd 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. 1st x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) ) )
15 brres 
 |-  ( x e. _V -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) ) )
16 15 elv 
 |-  ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) )
17 14 16 syl6rbbr 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> <. B , C >. 1st x ) )
18 br1steqg 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. 1st x <-> x = B ) )
19 17 18 bitrd 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> x = B ) )
20 19 3adant1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> x = B ) )
21 12 20 syl5bb 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( x `' ( 1st |` ( _V X. _V ) ) <. B , C >. <-> x = B ) )
22 21 anbi1cd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) <-> ( x = B /\ A R x ) ) )
23 22 exbidv 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x ( A R x /\ x `' ( 1st |` ( _V X. _V ) ) <. B , C >. ) <-> E. x ( x = B /\ A R x ) ) )
24 breq2 
 |-  ( x = B -> ( A R x <-> A R B ) )
25 24 ceqsexgv 
 |-  ( B e. W -> ( E. x ( x = B /\ A R x ) <-> A R B ) )
26 25 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x ( x = B /\ A R x ) <-> A R B ) )
27 9 23 26 3bitrd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. <-> A R B ) )
28 brcog 
 |-  ( ( A e. V /\ <. B , C >. e. _V ) -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) ) )
29 6 28 mpan2 
 |-  ( A e. V -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) ) )
30 29 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) ) )
31 brcnvg 
 |-  ( ( y e. _V /\ <. B , C >. e. _V ) -> ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 2nd |` ( _V X. _V ) ) y ) )
32 6 31 mpan2 
 |-  ( y e. _V -> ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 2nd |` ( _V X. _V ) ) y ) )
33 32 elv 
 |-  ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> <. B , C >. ( 2nd |` ( _V X. _V ) ) y )
34 13 biantrurd 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. 2nd y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) ) )
35 brres 
 |-  ( y e. _V -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) ) )
36 35 elv 
 |-  ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) )
37 34 36 syl6rbbr 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> <. B , C >. 2nd y ) )
38 br2ndeqg 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. 2nd y <-> y = C ) )
39 37 38 bitrd 
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> y = C ) )
40 39 3adant1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> y = C ) )
41 33 40 syl5bb 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. <-> y = C ) )
42 41 anbi1cd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) <-> ( y = C /\ A S y ) ) )
43 42 exbidv 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. y ( A S y /\ y `' ( 2nd |` ( _V X. _V ) ) <. B , C >. ) <-> E. y ( y = C /\ A S y ) ) )
44 breq2 
 |-  ( y = C -> ( A S y <-> A S C ) )
45 44 ceqsexgv 
 |-  ( C e. X -> ( E. y ( y = C /\ A S y ) <-> A S C ) )
46 45 3ad2ant3 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. y ( y = C /\ A S y ) <-> A S C ) )
47 30 43 46 3bitrd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. <-> A S C ) )
48 27 47 anbi12d 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ( `' ( 1st |` ( _V X. _V ) ) o. R ) <. B , C >. /\ A ( `' ( 2nd |` ( _V X. _V ) ) o. S ) <. B , C >. ) <-> ( A R B /\ A S C ) ) )
49 3 5 48 3bitrd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ( R |X. S ) <. B , C >. <-> ( A R B /\ A S C ) ) )