Metamath Proof Explorer


Theorem brxrn2

Description: A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020)

Ref Expression
Assertion brxrn2
|- ( A e. V -> ( A ( R |X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )

Proof

Step Hyp Ref Expression
1 xrnss3v
 |-  ( R |X. S ) C_ ( _V X. ( _V X. _V ) )
2 1 brel
 |-  ( A ( R |X. S ) B -> ( A e. _V /\ B e. ( _V X. _V ) ) )
3 2 simprd
 |-  ( A ( R |X. S ) B -> B e. ( _V X. _V ) )
4 elvv
 |-  ( B e. ( _V X. _V ) <-> E. x E. y B = <. x , y >. )
5 3 4 sylib
 |-  ( A ( R |X. S ) B -> E. x E. y B = <. x , y >. )
6 5 pm4.71ri
 |-  ( A ( R |X. S ) B <-> ( E. x E. y B = <. x , y >. /\ A ( R |X. S ) B ) )
7 19.41vv
 |-  ( E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) B ) <-> ( E. x E. y B = <. x , y >. /\ A ( R |X. S ) B ) )
8 breq2
 |-  ( B = <. x , y >. -> ( A ( R |X. S ) B <-> A ( R |X. S ) <. x , y >. ) )
9 8 pm5.32i
 |-  ( ( B = <. x , y >. /\ A ( R |X. S ) B ) <-> ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) )
10 9 2exbii
 |-  ( E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) B ) <-> E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) )
11 6 7 10 3bitr2i
 |-  ( A ( R |X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) )
12 brxrn
 |-  ( ( A e. V /\ x e. _V /\ y e. _V ) -> ( A ( R |X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) )
13 12 el3v23
 |-  ( A e. V -> ( A ( R |X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) )
14 13 anbi2d
 |-  ( A e. V -> ( ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) ) )
15 3anass
 |-  ( ( B = <. x , y >. /\ A R x /\ A S y ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) )
16 14 15 bitr4di
 |-  ( A e. V -> ( ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) <-> ( B = <. x , y >. /\ A R x /\ A S y ) ) )
17 16 2exbidv
 |-  ( A e. V -> ( E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )
18 11 17 syl5bb
 |-  ( A e. V -> ( A ( R |X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )