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