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 → X Y ∈ Pairs ⁡ V

Proof

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