Metamath Proof Explorer

Theorem sprval

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

Ref Expression
Assertion sprval ⊢ V ∈ W → Pairs ⁡ V = p | ∃ a ∈ V ∃ b ∈ V p = a b

Proof

Step Hyp Ref Expression
1 df-spr ⊢ Pairs = v ∈ V ⟼ p | ∃ a ∈ v ∃ b ∈ v p = a b
2 1 a1i ⊢ V ∈ W → Pairs = v ∈ V ⟼ p | ∃ a ∈ v ∃ b ∈ v p = a b
3 id ⊢ v = V → v = V
4 rexeq ⊢ v = V → ∃ b ∈ v p = a b ↔ ∃ b ∈ V p = a b
5 3 4 rexeqbidv ⊢ v = V → ∃ a ∈ v ∃ b ∈ v p = a b ↔ ∃ a ∈ V ∃ b ∈ V p = a b
6 5 adantl ⊢ V ∈ W ∧ v = V → ∃ a ∈ v ∃ b ∈ v p = a b ↔ ∃ a ∈ V ∃ b ∈ V p = a b
7 6 abbidv ⊢ V ∈ W ∧ v = V → p | ∃ a ∈ v ∃ b ∈ v p = a b = p | ∃ a ∈ V ∃ b ∈ V p = a b
8 elex ⊢ V ∈ W → V ∈ V
9 zfpair2 ⊢ a b ∈ V
10 eueq ⊢ a b ∈ V ↔ ∃! p p = a b
11 9 10 mpbi ⊢ ∃! p p = a b
12 euabex ⊢ ∃! p p = a b → p | p = a b ∈ V
13 11 12 mp1i ⊢ V ∈ W → p | p = a b ∈ V
14 13 ralrimivw ⊢ V ∈ W → ∀ b ∈ V p | p = a b ∈ V
15 abrexex2g ⊢ V ∈ W ∧ ∀ b ∈ V p | p = a b ∈ V → p | ∃ b ∈ V p = a b ∈ V
16 14 15 mpdan ⊢ V ∈ W → p | ∃ b ∈ V p = a b ∈ V
17 16 ralrimivw ⊢ V ∈ W → ∀ a ∈ V p | ∃ b ∈ V p = a b ∈ V
18 abrexex2g ⊢ V ∈ W ∧ ∀ a ∈ V p | ∃ b ∈ V p = a b ∈ V → p | ∃ a ∈ V ∃ b ∈ V p = a b ∈ V
19 17 18 mpdan ⊢ V ∈ W → p | ∃ a ∈ V ∃ b ∈ V p = a b ∈ V
20 2 7 8 19 fvmptd ⊢ V ∈ W → Pairs ⁡ V = p | ∃ a ∈ V ∃ b ∈ V p = a b