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∈Vp=ab
2 1 eqabrd ⊢V∈V→p∈Pairs⁡V↔∃a∈V∃b∈Vp=ab
3 2 anbi1d ⊢V∈V→p∈Pairs⁡V∧p=2↔∃a∈V∃b∈Vp=ab∧p=2
4 r19.41vv ⊢∃a∈V∃b∈Vp=ab∧p=2↔∃a∈V∃b∈Vp=ab∧p=2
5 fveqeq2 ⊢p=ab→p=2↔ab=2
6 hashprg ⊢a∈V∧b∈V→a≠b↔ab=2
7 6 el2v ⊢a≠b↔ab=2
8 5 7 bitr4di ⊢p=ab→p=2↔a≠b
9 8 pm5.32i ⊢p=ab∧p=2↔p=ab∧a≠b
10 9 biancomi ⊢p=ab∧p=2↔a≠b∧p=ab
11 10 a1i ⊢V∈V∧a∈V∧b∈V→p=ab∧p=2↔a≠b∧p=ab
12 11 2rexbidva ⊢V∈V→∃a∈V∃b∈Vp=ab∧p=2↔∃a∈V∃b∈Va≠b∧p=ab
13 4 12 bitr3id ⊢V∈V→∃a∈V∃b∈Vp=ab∧p=2↔∃a∈V∃b∈Va≠b∧p=ab
14 3 13 bitrd ⊢V∈V→p∈Pairs⁡V∧p=2↔∃a∈V∃b∈Va≠b∧p=ab
15 14 abbidv ⊢V∈V→p|p∈Pairs⁡V∧p=2=p|∃a∈V∃b∈Va≠b∧p=ab
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∈Va≠b∧p=ab
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