Metamath Proof Explorer

Theorem prproropreud

Description: There is exactly one ordered ordered pair fulfilling a wff iff there is exactly one proper pair fulfilling an equivalent wff. (Contributed by AV, 20-Mar-2023)

Ref Expression
Hypotheses prproropreud.o 
|- O = ( R i^i ( V X. V ) )
prproropreud.p 
|- P = { p e. ~P V | ( # ` p ) = 2 }
prproropreud.b 
|- ( ph -> R Or V )
prproropreud.x 
|- ( x = <. inf ( y , V , R ) , sup ( y , V , R ) >. -> ( ps <-> ch ) )
prproropreud.z 
|- ( x = z -> ( ps <-> th ) )
Assertion prproropreud 
|- ( ph -> ( E! x e. O ps <-> E! y e. P ch ) )

Proof

Step Hyp Ref Expression
1 prproropreud.o 
 |-  O = ( R i^i ( V X. V ) )
2 prproropreud.p 
 |-  P = { p e. ~P V | ( # ` p ) = 2 }
3 prproropreud.b 
 |-  ( ph -> R Or V )
4 prproropreud.x 
 |-  ( x = <. inf ( y , V , R ) , sup ( y , V , R ) >. -> ( ps <-> ch ) )
5 prproropreud.z 
 |-  ( x = z -> ( ps <-> th ) )
6 eqid 
 |-  ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) = ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. )
7 1 2 6 prproropf1o 
 |-  ( R Or V -> ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) : P -1-1-onto-> O )
8 3 7 syl 
 |-  ( ph -> ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) : P -1-1-onto-> O )
9 sbceq1a 
 |-  ( x = ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) -> ( ps <-> [. ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) / x ]. ps ) )
10 9 adantl 
 |-  ( ( ph /\ x = ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) ) -> ( ps <-> [. ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) / x ]. ps ) )
11 nfsbc1v 
 |-  F/ x [. ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) / x ]. ps
12 8 10 5 11 reuf1odnf 
 |-  ( ph -> ( E! x e. O ps <-> E! y e. P [. ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) / x ]. ps ) )
13 eqidd 
 |-  ( ( ph /\ y e. P ) -> ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) = ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) )
14 infeq1 
 |-  ( p = y -> inf ( p , V , R ) = inf ( y , V , R ) )
15 supeq1 
 |-  ( p = y -> sup ( p , V , R ) = sup ( y , V , R ) )
16 14 15 opeq12d 
 |-  ( p = y -> <. inf ( p , V , R ) , sup ( p , V , R ) >. = <. inf ( y , V , R ) , sup ( y , V , R ) >. )
17 16 adantl 
 |-  ( ( ( ph /\ y e. P ) /\ p = y ) -> <. inf ( p , V , R ) , sup ( p , V , R ) >. = <. inf ( y , V , R ) , sup ( y , V , R ) >. )
18 simpr 
 |-  ( ( ph /\ y e. P ) -> y e. P )
19 opex 
 |-  <. inf ( y , V , R ) , sup ( y , V , R ) >. e. _V
20 19 a1i 
 |-  ( ( ph /\ y e. P ) -> <. inf ( y , V , R ) , sup ( y , V , R ) >. e. _V )
21 13 17 18 20 fvmptd 
 |-  ( ( ph /\ y e. P ) -> ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) = <. inf ( y , V , R ) , sup ( y , V , R ) >. )
22 21 sbceq1d 
 |-  ( ( ph /\ y e. P ) -> ( [. ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) / x ]. ps <-> [. <. inf ( y , V , R ) , sup ( y , V , R ) >. / x ]. ps ) )
23 4 sbcieg 
 |-  ( <. inf ( y , V , R ) , sup ( y , V , R ) >. e. _V -> ( [. <. inf ( y , V , R ) , sup ( y , V , R ) >. / x ]. ps <-> ch ) )
24 20 23 syl 
 |-  ( ( ph /\ y e. P ) -> ( [. <. inf ( y , V , R ) , sup ( y , V , R ) >. / x ]. ps <-> ch ) )
25 22 24 bitrd 
 |-  ( ( ph /\ y e. P ) -> ( [. ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) / x ]. ps <-> ch ) )
26 25 reubidva 
 |-  ( ph -> ( E! y e. P [. ( ( p e. P |-> <. inf ( p , V , R ) , sup ( p , V , R ) >. ) ` y ) / x ]. ps <-> E! y e. P ch ) )
27 12 26 bitrd 
 |-  ( ph -> ( E! x e. O ps <-> E! y e. P ch ) )