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 )