This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem umgrbi

Description: Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021)

Ref Expression
Hypotheses umgrbi.x ⊢ X ∈ V
umgrbi.y ⊢ Y ∈ V
umgrbi.n ⊢ X ≠ Y
Assertion umgrbi ⊢ X Y ∈ x ∈ 𝒫 V | x = 2

Proof

Step Hyp Ref Expression
1 umgrbi.x ⊢ X ∈ V
2 umgrbi.y ⊢ Y ∈ V
3 umgrbi.n ⊢ X ≠ Y
4 prssi ⊢ X ∈ V ∧ Y ∈ V → X Y ⊆ V
5 1 2 4 mp2an ⊢ X Y ⊆ V
6 prex ⊢ X Y ∈ V
7 6 elpw ⊢ X Y ∈ 𝒫 V ↔ X Y ⊆ V
8 5 7 mpbir ⊢ X Y ∈ 𝒫 V
9 hashprg ⊢ X ∈ V ∧ Y ∈ V → X ≠ Y ↔ X Y = 2
10 3 9 mpbii ⊢ X ∈ V ∧ Y ∈ V → X Y = 2
11 1 2 10 mp2an ⊢ X Y = 2
12 fveqeq2 ⊢ x = X Y → x = 2 ↔ X Y = 2
13 12 elrab ⊢ X Y ∈ x ∈ 𝒫 V | x = 2 ↔ X Y ∈ 𝒫 V ∧ X Y = 2
14 8 11 13 mpbir2an ⊢ X Y ∈ x ∈ 𝒫 V | x = 2