This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem copsex2t

Description: Closed theorem form of copsex2g . (Contributed by NM, 17-Feb-2013)

Ref Expression
Assertion copsex2t 
|- ( ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) /\ ( A e. V /\ B e. W ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
2 nfe1 
 |-  F/ x E. x E. y ( <. A , B >. = <. x , y >. /\ ph )
3 nfv 
 |-  F/ x ps
4 2 3 nfbi 
 |-  F/ x ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps )
5 nfa2 
 |-  F/ y A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
6 nfe1 
 |-  F/ y E. y ( <. A , B >. = <. x , y >. /\ ph )
7 6 nfex 
 |-  F/ y E. x E. y ( <. A , B >. = <. x , y >. /\ ph )
8 nfv 
 |-  F/ y ps
9 7 8 nfbi 
 |-  F/ y ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps )
10 opeq12 
 |-  ( ( x = A /\ y = B ) -> <. x , y >. = <. A , B >. )
11 copsexgw 
 |-  ( <. A , B >. = <. x , y >. -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
12 11 eqcoms 
 |-  ( <. x , y >. = <. A , B >. -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
13 10 12 syl 
 |-  ( ( x = A /\ y = B ) -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
14 13 adantl 
 |-  ( ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) /\ ( x = A /\ y = B ) ) -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
15 2sp 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) -> ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) )
16 15 imp 
 |-  ( ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) /\ ( x = A /\ y = B ) ) -> ( ph <-> ps ) )
17 14 16 bitr3d 
 |-  ( ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) /\ ( x = A /\ y = B ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
18 17 ex 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) -> ( ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) ) )
19 5 9 18 exlimd 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) -> ( E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) ) )
20 1 4 19 exlimd 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) -> ( E. x E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) ) )
21 elisset 
 |-  ( A e. V -> E. x x = A )
22 elisset 
 |-  ( B e. W -> E. y y = B )
23 21 22 anim12i 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x x = A /\ E. y y = B ) )
24 exdistrv 
 |-  ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
25 23 24 sylibr 
 |-  ( ( A e. V /\ B e. W ) -> E. x E. y ( x = A /\ y = B ) )
26 20 25 impel 
 |-  ( ( A. x A. y ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) /\ ( A e. V /\ B e. W ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )