Metamath Proof Explorer

Theorem prelspr

Description: An unordered pair of elements of a fixed set V belongs to the set of all unordered pairs over the set V . (Contributed by AV, 21-Nov-2021)

Ref Expression
Assertion prelspr ⊢V∈W∧X∈V∧Y∈V→XY∈Pairs⁡V

Proof

Step Hyp Ref Expression
1 prelpwi ⊢X∈V∧Y∈V→XY∈𝒫V
2 eqidd ⊢X∈V∧Y∈V→XY=XY
3 preq1 ⊢a=X→ab=Xb
4 3 eqeq2d ⊢a=X→XY=ab↔XY=Xb
5 preq2 ⊢b=Y→Xb=XY
6 5 eqeq2d ⊢b=Y→XY=Xb↔XY=XY
7 4 6 rspc2ev ⊢X∈V∧Y∈V∧XY=XY→∃a∈V∃b∈VXY=ab
8 2 7 mpd3an3 ⊢X∈V∧Y∈V→∃a∈V∃b∈VXY=ab
9 1 8 jca ⊢X∈V∧Y∈V→XY∈𝒫V∧∃a∈V∃b∈VXY=ab
10 9 adantl ⊢V∈W∧X∈V∧Y∈V→XY∈𝒫V∧∃a∈V∃b∈VXY=ab
11 eqeq1 ⊢p=XY→p=ab↔XY=ab
12 11 2rexbidv ⊢p=XY→∃a∈V∃b∈Vp=ab↔∃a∈V∃b∈VXY=ab
13 12 elrab ⊢XY∈p∈𝒫V|∃a∈V∃b∈Vp=ab↔XY∈𝒫V∧∃a∈V∃b∈VXY=ab
14 10 13 sylibr ⊢V∈W∧X∈V∧Y∈V→XY∈p∈𝒫V|∃a∈V∃b∈Vp=ab
15 sprvalpw ⊢V∈W→Pairs⁡V=p∈𝒫V|∃a∈V∃b∈Vp=ab
16 15 adantr ⊢V∈W∧X∈V∧Y∈V→Pairs⁡V=p∈𝒫V|∃a∈V∃b∈Vp=ab
17 14 16 eleqtrrd ⊢V∈W∧X∈V∧Y∈V→XY∈Pairs⁡V