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