Metamath Proof Explorer

Theorem prprspr2

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

Ref Expression
Assertion prprspr2 ⊢ PrPairs ⁡ V = p ∈ Pairs ⁡ V | p = 2

Proof

Step Hyp Ref Expression
1 sprval ⊢ V ∈ V → Pairs ⁡ V = p | ∃ a ∈ V ∃ b ∈ V p = a b
2 1 abeq2d ⊢ V ∈ V → p ∈ Pairs ⁡ V ↔ ∃ a ∈ V ∃ b ∈ V p = a b
3 2 anbi1d ⊢ V ∈ V → p ∈ Pairs ⁡ V ∧ p = 2 ↔ ∃ a ∈ V ∃ b ∈ V p = a b ∧ p = 2
4 r19.41vv ⊢ ∃ a ∈ V ∃ b ∈ V p = a b ∧ p = 2 ↔ ∃ a ∈ V ∃ b ∈ V p = a b ∧ p = 2
5 fveqeq2 ⊢ p = a b → p = 2 ↔ a b = 2
6 hashprg ⊢ a ∈ V ∧ b ∈ V → a ≠ b ↔ a b = 2
7 6 el2v ⊢ a ≠ b ↔ a b = 2
8 5 7 syl6bbr ⊢ p = a b → p = 2 ↔ a ≠ b
9 8 pm5.32i ⊢ p = a b ∧ p = 2 ↔ p = a b ∧ a ≠ b
10 9 biancomi ⊢ p = a b ∧ p = 2 ↔ a ≠ b ∧ p = a b
11 10 a1i ⊢ V ∈ V ∧ a ∈ V ∧ b ∈ V → p = a b ∧ p = 2 ↔ a ≠ b ∧ p = a b
12 11 2rexbidva ⊢ V ∈ V → ∃ a ∈ V ∃ b ∈ V p = a b ∧ p = 2 ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
13 4 12 syl5bbr ⊢ V ∈ V → ∃ a ∈ V ∃ b ∈ V p = a b ∧ p = 2 ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
14 3 13 bitrd ⊢ V ∈ V → p ∈ Pairs ⁡ V ∧ p = 2 ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
15 14 abbidv ⊢ V ∈ V → p | p ∈ Pairs ⁡ V ∧ p = 2 = p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
16 df-rab ⊢ p ∈ Pairs ⁡ V | p = 2 = p | p ∈ Pairs ⁡ V ∧ p = 2
17 16 a1i ⊢ V ∈ V → p ∈ Pairs ⁡ V | p = 2 = p | p ∈ Pairs ⁡ V ∧ p = 2
18 prprval ⊢ V ∈ V → PrPairs ⁡ V = p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
19 15 17 18 3eqtr4rd ⊢ V ∈ V → PrPairs ⁡ V = p ∈ Pairs ⁡ V | p = 2
20 rab0 ⊢ p ∈ ∅ | p = 2 = ∅
21 20 a1i ⊢ ¬ V ∈ V → p ∈ ∅ | p = 2 = ∅
22 fvprc ⊢ ¬ V ∈ V → Pairs ⁡ V = ∅
23 22 rabeqdv ⊢ ¬ V ∈ V → p ∈ Pairs ⁡ V | p = 2 = p ∈ ∅ | p = 2
24 fvprc ⊢ ¬ V ∈ V → PrPairs ⁡ V = ∅
25 21 23 24 3eqtr4rd ⊢ ¬ V ∈ V → PrPairs ⁡ V = p ∈ Pairs ⁡ V | p = 2
26 19 25 pm2.61i ⊢ PrPairs ⁡ V = p ∈ Pairs ⁡ V | p = 2