Metamath Proof Explorer

Theorem eloprab1st2nd

Description: Reconstruction of a nested ordered pair in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion eloprab1st2nd 
|- ( A e. { <. <. x , y >. , z >. | ph } -> A = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( w = A -> ( w = <. <. x , y >. , z >. <-> A = <. <. x , y >. , z >. ) )
2 1 anbi1d 
 |-  ( w = A -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( A = <. <. x , y >. , z >. /\ ph ) ) )
3 2 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 ) ) )
4 df-oprab 
 |-  { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
5 3 4 elab2g 
 |-  ( A e. { <. <. x , y >. , z >. | ph } -> ( A e. { <. <. x , y >. , z >. | ph } <-> E. x E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) ) )
6 5 ibi 
 |-  ( A e. { <. <. x , y >. , z >. | ph } -> E. x E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) )
7 id 
 |-  ( A = <. <. x , y >. , z >. -> A = <. <. x , y >. , z >. )
8 opex 
 |-  <. x , y >. e. _V
9 vex 
 |-  z e. _V
10 8 9 op1std 
 |-  ( A = <. <. x , y >. , z >. -> ( 1st ` A ) = <. x , y >. )
11 10 fveq2d 
 |-  ( A = <. <. x , y >. , z >. -> ( 1st ` ( 1st ` A ) ) = ( 1st ` <. x , y >. ) )
12 vex 
 |-  x e. _V
13 vex 
 |-  y e. _V
14 12 13 op1st 
 |-  ( 1st ` <. x , y >. ) = x
15 11 14 eqtr2di 
 |-  ( A = <. <. x , y >. , z >. -> x = ( 1st ` ( 1st ` A ) ) )
16 10 fveq2d 
 |-  ( A = <. <. x , y >. , z >. -> ( 2nd ` ( 1st ` A ) ) = ( 2nd ` <. x , y >. ) )
17 12 13 op2nd 
 |-  ( 2nd ` <. x , y >. ) = y
18 16 17 eqtr2di 
 |-  ( A = <. <. x , y >. , z >. -> y = ( 2nd ` ( 1st ` A ) ) )
19 15 18 opeq12d 
 |-  ( A = <. <. x , y >. , z >. -> <. x , y >. = <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. )
20 8 9 op2ndd 
 |-  ( A = <. <. x , y >. , z >. -> ( 2nd ` A ) = z )
21 20 eqcomd 
 |-  ( A = <. <. x , y >. , z >. -> z = ( 2nd ` A ) )
22 19 21 opeq12d 
 |-  ( A = <. <. x , y >. , z >. -> <. <. x , y >. , z >. = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )
23 7 22 eqtrd 
 |-  ( A = <. <. x , y >. , z >. -> A = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )
24 23 adantr 
 |-  ( ( A = <. <. x , y >. , z >. /\ ph ) -> A = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )
25 24 exlimiv 
 |-  ( E. z ( A = <. <. x , y >. , z >. /\ ph ) -> A = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )
26 25 exlimivv 
 |-  ( E. x E. y E. z ( A = <. <. x , y >. , z >. /\ ph ) -> A = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )
27 6 26 syl 
 |-  ( A e. { <. <. x , y >. , z >. | ph } -> A = <. <. ( 1st ` ( 1st ` A ) ) , ( 2nd ` ( 1st ` A ) ) >. , ( 2nd ` A ) >. )