Metamath Proof Explorer

Theorem sprssspr

Description: The set of all unordered pairs over a given set V is a subset of the set of all unordered pairs. (Contributed by AV, 21-Nov-2021)

Ref Expression
Assertion sprssspr ⊢Pairs⁡V⊆p|∃a∃bp=ab

Proof

Step Hyp Ref Expression
1 sprval ⊢V∈V→Pairs⁡V=p|∃a∈V∃b∈Vp=ab
2 r2ex ⊢∃a∈V∃b∈Vp=ab↔∃a∃ba∈V∧b∈V∧p=ab
3 simpr ⊢a∈V∧b∈V∧p=ab→p=ab
4 3 2eximi ⊢∃a∃ba∈V∧b∈V∧p=ab→∃a∃bp=ab
5 2 4 sylbi ⊢∃a∈V∃b∈Vp=ab→∃a∃bp=ab
6 5 ax-gen ⊢∀p∃a∈V∃b∈Vp=ab→∃a∃bp=ab
7 6 a1i ⊢V∈V→∀p∃a∈V∃b∈Vp=ab→∃a∃bp=ab
8 ss2ab ⊢p|∃a∈V∃b∈Vp=ab⊆p|∃a∃bp=ab↔∀p∃a∈V∃b∈Vp=ab→∃a∃bp=ab
9 7 8 sylibr ⊢V∈V→p|∃a∈V∃b∈Vp=ab⊆p|∃a∃bp=ab
10 1 9 eqsstrd ⊢V∈V→Pairs⁡V⊆p|∃a∃bp=ab
11 fvprc ⊢¬V∈V→Pairs⁡V=∅
12 0ss ⊢∅⊆p|∃a∃bp=ab
13 12 a1i ⊢¬V∈V→∅⊆p|∃a∃bp=ab
14 11 13 eqsstrd ⊢¬V∈V→Pairs⁡V⊆p|∃a∃bp=ab
15 10 14 pm2.61i ⊢Pairs⁡V⊆p|∃a∃bp=ab