Metamath Proof Explorer

Theorem prprelb

Description: An element of the set of all proper unordered pairs over a given set V is a subset of V of size two. (Contributed by AV, 29-Apr-2023)

Ref Expression
Assertion prprelb ⊢ V ∈ W → P ∈ PrPairs ⁡ V ↔ P ∈ 𝒫 V ∧ P = 2

Proof

Step Hyp Ref Expression
1 prprvalpw ⊢ V ∈ W → PrPairs ⁡ V = p ∈ 𝒫 V | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
2 1 eleq2d ⊢ V ∈ W → P ∈ PrPairs ⁡ V ↔ P ∈ p ∈ 𝒫 V | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
3 eqeq1 ⊢ p = P → p = a b ↔ P = a b
4 3 anbi2d ⊢ p = P → a ≠ b ∧ p = a b ↔ a ≠ b ∧ P = a b
5 4 2rexbidv ⊢ p = P → ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b
6 5 elrab ⊢ P ∈ p ∈ 𝒫 V | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b ↔ P ∈ 𝒫 V ∧ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b
7 2 6 bitrdi ⊢ V ∈ W → P ∈ PrPairs ⁡ V ↔ P ∈ 𝒫 V ∧ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b
8 hash2exprb ⊢ P ∈ 𝒫 V → P = 2 ↔ ∃ a ∃ b a ≠ b ∧ P = a b
9 eleq1 ⊢ P = a b → P ∈ 𝒫 V ↔ a b ∈ 𝒫 V
10 prelpw ⊢ a ∈ V ∧ b ∈ V → a ∈ V ∧ b ∈ V ↔ a b ∈ 𝒫 V
11 10 el2v ⊢ a ∈ V ∧ b ∈ V ↔ a b ∈ 𝒫 V
12 11 biimpri ⊢ a b ∈ 𝒫 V → a ∈ V ∧ b ∈ V
13 9 12 syl6bi ⊢ P = a b → P ∈ 𝒫 V → a ∈ V ∧ b ∈ V
14 13 com12 ⊢ P ∈ 𝒫 V → P = a b → a ∈ V ∧ b ∈ V
15 14 adantld ⊢ P ∈ 𝒫 V → a ≠ b ∧ P = a b → a ∈ V ∧ b ∈ V
16 15 pm4.71rd ⊢ P ∈ 𝒫 V → a ≠ b ∧ P = a b ↔ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ P = a b
17 16 2exbidv ⊢ P ∈ 𝒫 V → ∃ a ∃ b a ≠ b ∧ P = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ P = a b
18 r2ex ⊢ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ P = a b
19 17 18 bitr4di ⊢ P ∈ 𝒫 V → ∃ a ∃ b a ≠ b ∧ P = a b ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b
20 8 19 bitr2d ⊢ P ∈ 𝒫 V → ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b ↔ P = 2
21 20 pm5.32i ⊢ P ∈ 𝒫 V ∧ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b ↔ P ∈ 𝒫 V ∧ P = 2
22 7 21 bitrdi ⊢ V ∈ W → P ∈ PrPairs ⁡ V ↔ P ∈ 𝒫 V ∧ P = 2