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 brres
 |-  ( x e. _V -> ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) ) )
14 13 elv
 |-  ( <. B , C >. ( 1st |` ( _V X. _V ) ) x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) )
15 opelvvg
 |-  ( ( B e. W /\ C e. X ) -> <. B , C >. e. ( _V X. _V ) )
16 15 biantrurd
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. 1st x <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 1st x ) ) )
17 14 16 bitr4id
 |-  ( ( 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 brres
 |-  ( y e. _V -> ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) ) )
35 34 elv
 |-  ( <. B , C >. ( 2nd |` ( _V X. _V ) ) y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) )
36 15 biantrurd
 |-  ( ( B e. W /\ C e. X ) -> ( <. B , C >. 2nd y <-> ( <. B , C >. e. ( _V X. _V ) /\ <. B , C >. 2nd y ) ) )
37 35 36 bitr4id
 |-  ( ( 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 ) ) )