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 }