Metamath Proof Explorer

Theorem eloprabi

Description: A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypotheses eloprabi.1 
|- ( x = ( 1st ` ( 1st ` A ) ) -> ( ph <-> ps ) )
eloprabi.2 
|- ( y = ( 2nd ` ( 1st ` A ) ) -> ( ps <-> ch ) )
eloprabi.3 
|- ( z = ( 2nd ` A ) -> ( ch <-> th ) )
Assertion eloprabi 
|- ( A e. { <. <. x , y >. , z >. | ph } -> th )

Proof

Step Hyp Ref Expression
1 eloprabi.1 
 |-  ( x = ( 1st ` ( 1st ` A ) ) -> ( ph <-> ps ) )
2 eloprabi.2 
 |-  ( y = ( 2nd ` ( 1st ` A ) ) -> ( ps <-> ch ) )
3 eloprabi.3 
 |-  ( z = ( 2nd ` A ) -> ( ch <-> th ) )
4 eqeq1 
 |-  ( w = A -> ( w = <. <. x , y >. , z >. <-> A = <. <. x , y >. , z >. ) )
5 4 anbi1d 
 |-  ( w = A -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( A = <. <. x , y >. , z >. /\ ph ) ) )
6 5 3exbidv 
 |-  ( w = A -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> E. x E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) ) )
7 df-oprab 
 |-  { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
8 6 7 elab2g 
 |-  ( A e. { <. <. x , y >. , z >. | ph } -> ( A e. { <. <. x , y >. , z >. | ph } <-> E. x E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) ) )
9 8 ibi 
 |-  ( A e. { <. <. x , y >. , z >. | ph } -> E. x E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) )
10 opex 
 |-  <. x , y >. e. _V
11 vex 
 |-  z e. _V
12 10 11 op1std 
 |-  ( A = <. <. x , y >. , z >. -> ( 1st ` A ) = <. x , y >. )
13 12 fveq2d 
 |-  ( A = <. <. x , y >. , z >. -> ( 1st ` ( 1st ` A ) ) = ( 1st ` <. x , y >. ) )
14 vex 
 |-  x e. _V
15 vex 
 |-  y e. _V
16 14 15 op1st 
 |-  ( 1st ` <. x , y >. ) = x
17 13 16 eqtr2di 
 |-  ( A = <. <. x , y >. , z >. -> x = ( 1st ` ( 1st ` A ) ) )
18 17 1 syl 
 |-  ( A = <. <. x , y >. , z >. -> ( ph <-> ps ) )
19 12 fveq2d 
 |-  ( A = <. <. x , y >. , z >. -> ( 2nd ` ( 1st ` A ) ) = ( 2nd ` <. x , y >. ) )
20 14 15 op2nd 
 |-  ( 2nd ` <. x , y >. ) = y
21 19 20 eqtr2di 
 |-  ( A = <. <. x , y >. , z >. -> y = ( 2nd ` ( 1st ` A ) ) )
22 21 2 syl 
 |-  ( A = <. <. x , y >. , z >. -> ( ps <-> ch ) )
23 10 11 op2ndd 
 |-  ( A = <. <. x , y >. , z >. -> ( 2nd ` A ) = z )
24 23 eqcomd 
 |-  ( A = <. <. x , y >. , z >. -> z = ( 2nd ` A ) )
25 24 3 syl 
 |-  ( A = <. <. x , y >. , z >. -> ( ch <-> th ) )
26 18 22 25 3bitrd 
 |-  ( A = <. <. x , y >. , z >. -> ( ph <-> th ) )
27 26 biimpa 
 |-  ( ( A = <. <. x , y >. , z >. /\ ph ) -> th )
28 27 exlimiv 
 |-  ( E. z ( A = <. <. x , y >. , z >. /\ ph ) -> th )
29 28 exlimiv 
 |-  ( E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) -> th )
30 29 exlimiv 
 |-  ( E. x E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) -> th )
31 9 30 syl 
 |-  ( A e. { <. <. x , y >. , z >. | ph } -> th )