Metamath Proof Explorer


Theorem cnvoprab

Description: The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017) (Proof shortened by Thierry Arnoux, 20-Feb-2022)

Ref Expression
Hypotheses cnvoprab.1
|- ( a = <. x , y >. -> ( ps <-> ph ) )
cnvoprab.2
|- ( ps -> a e. ( _V X. _V ) )
Assertion cnvoprab
|- `' { <. <. x , y >. , z >. | ph } = { <. z , a >. | ps }

Proof

Step Hyp Ref Expression
1 cnvoprab.1
 |-  ( a = <. x , y >. -> ( ps <-> ph ) )
2 cnvoprab.2
 |-  ( ps -> a e. ( _V X. _V ) )
3 1 dfoprab3
 |-  { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = { <. <. x , y >. , z >. | ph }
4 3 cnveqi
 |-  `' { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = `' { <. <. x , y >. , z >. | ph }
5 cnvopab
 |-  `' { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = { <. z , a >. | ( a e. ( _V X. _V ) /\ ps ) }
6 inopab
 |-  ( { <. z , a >. | a e. ( _V X. _V ) } i^i { <. z , a >. | ps } ) = { <. z , a >. | ( a e. ( _V X. _V ) /\ ps ) }
7 2 ssopab2i
 |-  { <. z , a >. | ps } C_ { <. z , a >. | a e. ( _V X. _V ) }
8 sseqin2
 |-  ( { <. z , a >. | ps } C_ { <. z , a >. | a e. ( _V X. _V ) } <-> ( { <. z , a >. | a e. ( _V X. _V ) } i^i { <. z , a >. | ps } ) = { <. z , a >. | ps } )
9 7 8 mpbi
 |-  ( { <. z , a >. | a e. ( _V X. _V ) } i^i { <. z , a >. | ps } ) = { <. z , a >. | ps }
10 5 6 9 3eqtr2i
 |-  `' { <. a , z >. | ( a e. ( _V X. _V ) /\ ps ) } = { <. z , a >. | ps }
11 4 10 eqtr3i
 |-  `' { <. <. x , y >. , z >. | ph } = { <. z , a >. | ps }