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 imbitrdi 
 |-  ( 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 ) )