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

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 }