Step |
Hyp |
Ref |
Expression |
1 |
|
ecoptocl.1 |
|- S = ( ( B X. C ) /. R ) |
2 |
|
ecoptocl.2 |
|- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) ) |
3 |
|
ecoptocl.3 |
|- ( ( x e. B /\ y e. C ) -> ph ) |
4 |
|
elqsi |
|- ( A e. ( ( B X. C ) /. R ) -> E. z e. ( B X. C ) A = [ z ] R ) |
5 |
|
eqid |
|- ( B X. C ) = ( B X. C ) |
6 |
|
eceq1 |
|- ( <. x , y >. = z -> [ <. x , y >. ] R = [ z ] R ) |
7 |
6
|
eqeq2d |
|- ( <. x , y >. = z -> ( A = [ <. x , y >. ] R <-> A = [ z ] R ) ) |
8 |
7
|
imbi1d |
|- ( <. x , y >. = z -> ( ( A = [ <. x , y >. ] R -> ps ) <-> ( A = [ z ] R -> ps ) ) ) |
9 |
2
|
eqcoms |
|- ( A = [ <. x , y >. ] R -> ( ph <-> ps ) ) |
10 |
3 9
|
syl5ibcom |
|- ( ( x e. B /\ y e. C ) -> ( A = [ <. x , y >. ] R -> ps ) ) |
11 |
5 8 10
|
optocl |
|- ( z e. ( B X. C ) -> ( A = [ z ] R -> ps ) ) |
12 |
11
|
rexlimiv |
|- ( E. z e. ( B X. C ) A = [ z ] R -> ps ) |
13 |
4 12
|
syl |
|- ( A e. ( ( B X. C ) /. R ) -> ps ) |
14 |
13 1
|
eleq2s |
|- ( A e. S -> ps ) |