Metamath Proof Explorer

Theorem prprval

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

Ref Expression
Assertion prprval ⊢ V ∈ W → PrPairs ⁡ V = p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b

Proof

Step Hyp Ref Expression
1 df-prpr ⊢ PrPairs = v ∈ V ⟼ p | ∃ a ∈ v ∃ b ∈ v a ≠ b ∧ p = a b
2 rexeq ⊢ v = V → ∃ b ∈ v a ≠ b ∧ p = a b ↔ ∃ b ∈ V a ≠ b ∧ p = a b
3 2 rexeqbi1dv ⊢ v = V → ∃ a ∈ v ∃ b ∈ v a ≠ b ∧ p = a b ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
4 3 abbidv ⊢ v = V → p | ∃ a ∈ v ∃ b ∈ v a ≠ b ∧ p = a b = p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
5 4 adantl ⊢ V ∈ W ∧ v = V → p | ∃ a ∈ v ∃ b ∈ v a ≠ b ∧ p = a b = p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b
6 elex ⊢ V ∈ W → V ∈ V
7 simpr ⊢ a ≠ b ∧ p = a b → p = a b
8 7 ss2abi ⊢ p | a ≠ b ∧ p = a b ⊆ p | p = a b
9 zfpair2 ⊢ a b ∈ V
10 9 eueqi ⊢ ∃! p p = a b
11 euabex ⊢ ∃! p p = a b → p | p = a b ∈ V
12 10 11 mp1i ⊢ V ∈ W → p | p = a b ∈ V
13 ssexg ⊢ p | a ≠ b ∧ p = a b ⊆ p | p = a b ∧ p | p = a b ∈ V → p | a ≠ b ∧ p = a b ∈ V
14 8 12 13 sylancr ⊢ V ∈ W → p | a ≠ b ∧ p = a b ∈ V
15 14 ralrimivw ⊢ V ∈ W → ∀ b ∈ V p | a ≠ b ∧ p = a b ∈ V
16 abrexex2g ⊢ V ∈ W ∧ ∀ b ∈ V p | a ≠ b ∧ p = a b ∈ V → p | ∃ b ∈ V a ≠ b ∧ p = a b ∈ V
17 15 16 mpdan ⊢ V ∈ W → p | ∃ b ∈ V a ≠ b ∧ p = a b ∈ V
18 17 ralrimivw ⊢ V ∈ W → ∀ a ∈ V p | ∃ b ∈ V a ≠ b ∧ p = a b ∈ V
19 abrexex2g ⊢ V ∈ W ∧ ∀ a ∈ V p | ∃ b ∈ V a ≠ b ∧ p = a b ∈ V → p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b ∈ V
20 18 19 mpdan ⊢ V ∈ W → p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b ∈ V
21 1 5 6 20 fvmptd2 ⊢ V ∈ W → PrPairs ⁡ V = p | ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ p = a b