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∈Va≠b∧p=ab

Proof

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