Metamath Proof Explorer


Theorem elinxp

Description: Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elinxp
|- ( C e. ( R i^i ( A X. B ) ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ <. x , y >. e. R ) )

Proof

Step Hyp Ref Expression
1 relinxp
 |-  Rel ( R i^i ( A X. B ) )
2 elrel
 |-  ( ( Rel ( R i^i ( A X. B ) ) /\ C e. ( R i^i ( A X. B ) ) ) -> E. x E. y C = <. x , y >. )
3 1 2 mpan
 |-  ( C e. ( R i^i ( A X. B ) ) -> E. x E. y C = <. x , y >. )
4 eleq1
 |-  ( C = <. x , y >. -> ( C e. ( R i^i ( A X. B ) ) <-> <. x , y >. e. ( R i^i ( A X. B ) ) ) )
5 4 biimpd
 |-  ( C = <. x , y >. -> ( C e. ( R i^i ( A X. B ) ) -> <. x , y >. e. ( R i^i ( A X. B ) ) ) )
6 opelinxp
 |-  ( <. x , y >. e. ( R i^i ( A X. B ) ) <-> ( ( x e. A /\ y e. B ) /\ <. x , y >. e. R ) )
7 6 biimpi
 |-  ( <. x , y >. e. ( R i^i ( A X. B ) ) -> ( ( x e. A /\ y e. B ) /\ <. x , y >. e. R ) )
8 5 7 syl6com
 |-  ( C e. ( R i^i ( A X. B ) ) -> ( C = <. x , y >. -> ( ( x e. A /\ y e. B ) /\ <. x , y >. e. R ) ) )
9 8 ancld
 |-  ( C e. ( R i^i ( A X. B ) ) -> ( C = <. x , y >. -> ( C = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ <. x , y >. e. R ) ) ) )
10 an12
 |-  ( ( C = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ <. x , y >. e. R ) ) <-> ( ( x e. A /\ y e. B ) /\ ( C = <. x , y >. /\ <. x , y >. e. R ) ) )
11 9 10 syl6ib
 |-  ( C e. ( R i^i ( A X. B ) ) -> ( C = <. x , y >. -> ( ( x e. A /\ y e. B ) /\ ( C = <. x , y >. /\ <. x , y >. e. R ) ) ) )
12 11 2eximdv
 |-  ( C e. ( R i^i ( A X. B ) ) -> ( E. x E. y C = <. x , y >. -> E. x E. y ( ( x e. A /\ y e. B ) /\ ( C = <. x , y >. /\ <. x , y >. e. R ) ) ) )
13 3 12 mpd
 |-  ( C e. ( R i^i ( A X. B ) ) -> E. x E. y ( ( x e. A /\ y e. B ) /\ ( C = <. x , y >. /\ <. x , y >. e. R ) ) )
14 r2ex
 |-  ( E. x e. A E. y e. B ( C = <. x , y >. /\ <. x , y >. e. R ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ( C = <. x , y >. /\ <. x , y >. e. R ) ) )
15 13 14 sylibr
 |-  ( C e. ( R i^i ( A X. B ) ) -> E. x e. A E. y e. B ( C = <. x , y >. /\ <. x , y >. e. R ) )
16 6 simplbi2
 |-  ( ( x e. A /\ y e. B ) -> ( <. x , y >. e. R -> <. x , y >. e. ( R i^i ( A X. B ) ) ) )
17 4 biimprd
 |-  ( C = <. x , y >. -> ( <. x , y >. e. ( R i^i ( A X. B ) ) -> C e. ( R i^i ( A X. B ) ) ) )
18 16 17 syl9
 |-  ( ( x e. A /\ y e. B ) -> ( C = <. x , y >. -> ( <. x , y >. e. R -> C e. ( R i^i ( A X. B ) ) ) ) )
19 18 impd
 |-  ( ( x e. A /\ y e. B ) -> ( ( C = <. x , y >. /\ <. x , y >. e. R ) -> C e. ( R i^i ( A X. B ) ) ) )
20 19 rexlimivv
 |-  ( E. x e. A E. y e. B ( C = <. x , y >. /\ <. x , y >. e. R ) -> C e. ( R i^i ( A X. B ) ) )
21 15 20 impbii
 |-  ( C e. ( R i^i ( A X. B ) ) <-> E. x e. A E. y e. B ( C = <. x , y >. /\ <. x , y >. e. R ) )