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=RV×V
prproropreud.p P=p𝒫V|p=2
prproropreud.b φROrV
prproropreud.x x=supyVRsupyVRψχ
prproropreud.z x=zψθ
Assertion prproropreud φ∃!xOψ∃!yPχ

Proof

Step Hyp Ref Expression
1 prproropreud.o O=RV×V
2 prproropreud.p P=p𝒫V|p=2
3 prproropreud.b φROrV
4 prproropreud.x x=supyVRsupyVRψχ
5 prproropreud.z x=zψθ
6 eqid pPsuppVRsuppVR=pPsuppVRsuppVR
7 1 2 6 prproropf1o ROrVpPsuppVRsuppVR:P1-1 ontoO
8 3 7 syl φpPsuppVRsuppVR:P1-1 ontoO
9 sbceq1a x=pPsuppVRsuppVRyψ[˙pPsuppVRsuppVRy/x]˙ψ
10 9 adantl φx=pPsuppVRsuppVRyψ[˙pPsuppVRsuppVRy/x]˙ψ
11 nfsbc1v x[˙pPsuppVRsuppVRy/x]˙ψ
12 8 10 5 11 reuf1odnf φ∃!xOψ∃!yP[˙pPsuppVRsuppVRy/x]˙ψ
13 eqidd φyPpPsuppVRsuppVR=pPsuppVRsuppVR
14 infeq1 p=ysuppVR=supyVR
15 supeq1 p=ysuppVR=supyVR
16 14 15 opeq12d p=ysuppVRsuppVR=supyVRsupyVR
17 16 adantl φyPp=ysuppVRsuppVR=supyVRsupyVR
18 simpr φyPyP
19 opex supyVRsupyVRV
20 19 a1i φyPsupyVRsupyVRV
21 13 17 18 20 fvmptd φyPpPsuppVRsuppVRy=supyVRsupyVR
22 21 sbceq1d φyP[˙pPsuppVRsuppVRy/x]˙ψ[˙supyVRsupyVR/x]˙ψ
23 4 sbcieg supyVRsupyVRV[˙supyVRsupyVR/x]˙ψχ
24 20 23 syl φyP[˙supyVRsupyVR/x]˙ψχ
25 22 24 bitrd φyP[˙pPsuppVRsuppVRy/x]˙ψχ
26 25 reubidva φ∃!yP[˙pPsuppVRsuppVRy/x]˙ψ∃!yPχ
27 12 26 bitrd φ∃!xOψ∃!yPχ