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 ∩ V × V
prproropreud.p ⊢ P = p ∈ 𝒫 V | p = 2
prproropreud.b ⊢ φ → R Or V
prproropreud.x ⊢ x = inf y V R sup y V R → ψ ↔ χ
prproropreud.z ⊢ x = z → ψ ↔ θ
Assertion prproropreud ⊢ φ → ∃! x ∈ O ψ ↔ ∃! y ∈ P χ

Proof

Step Hyp Ref Expression
1 prproropreud.o ⊢ O = R ∩ V × V
2 prproropreud.p ⊢ P = p ∈ 𝒫 V | p = 2
3 prproropreud.b ⊢ φ → R Or V
4 prproropreud.x ⊢ x = inf y V R sup y V R → ψ ↔ χ
5 prproropreud.z ⊢ x = z → ψ ↔ θ
6 eqid ⊢ p ∈ P ⟼ inf p V R sup p V R = p ∈ P ⟼ inf p V R sup p V R
7 1 2 6 prproropf1o ⊢ R Or V → p ∈ P ⟼ inf p V R sup p V R : P ⟶ 1-1 onto O
8 3 7 syl ⊢ φ → p ∈ P ⟼ inf p V R sup p V R : P ⟶ 1-1 onto O
9 sbceq1a ⊢ x = p ∈ P ⟼ inf p V R sup p V R ⁡ y → ψ ↔ [˙ p ∈ P ⟼ inf p V R sup p V R ⁡ y / x]˙ ψ
10 9 adantl ⊢ φ ∧ x = p ∈ P ⟼ inf p V R sup p V R ⁡ y → ψ ↔ [˙ p ∈ P ⟼ inf p V R sup p V R ⁡ y / x]˙ ψ
11 nfsbc1v ⊢ Ⅎ x [˙ p ∈ P ⟼ inf p V R sup p V R ⁡ y / x]˙ ψ
12 8 10 5 11 reuf1odnf ⊢ φ → ∃! x ∈ O ψ ↔ ∃! y ∈ P [˙ p ∈ P ⟼ inf p V R sup p V R ⁡ y / x]˙ ψ
13 eqidd ⊢ φ ∧ y ∈ P → p ∈ P ⟼ inf p V R sup p V R = p ∈ 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 ⊢ φ ∧ y ∈ P ∧ p = y → inf p V R sup p V R = inf y V R sup y V R
18 simpr ⊢ φ ∧ y ∈ P → y ∈ P
19 opex ⊢ inf y V R sup y V R ∈ V
20 19 a1i ⊢ φ ∧ y ∈ P → inf y V R sup y V R ∈ V
21 13 17 18 20 fvmptd ⊢ φ ∧ y ∈ P → p ∈ P ⟼ inf p V R sup p V R ⁡ y = inf y V R sup y V R
22 21 sbceq1d ⊢ φ ∧ y ∈ P → [˙ p ∈ P ⟼ inf p V R sup p V R ⁡ y / x]˙ ψ ↔ [˙ inf y V R sup y V R / x]˙ ψ
23 4 sbcieg ⊢ inf y V R sup y V R ∈ V → [˙ inf y V R sup y V R / x]˙ ψ ↔ χ
24 20 23 syl ⊢ φ ∧ y ∈ P → [˙ inf y V R sup y V R / x]˙ ψ ↔ χ
25 22 24 bitrd ⊢ φ ∧ y ∈ P → [˙ p ∈ P ⟼ inf p V R sup p V R ⁡ y / x]˙ ψ ↔ χ
26 25 reubidva ⊢ φ → ∃! y ∈ P [˙ p ∈ P ⟼ inf p V R sup p V R ⁡ y / x]˙ ψ ↔ ∃! y ∈ P χ
27 12 26 bitrd ⊢ φ → ∃! x ∈ O ψ ↔ ∃! y ∈ P χ