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 ⊢ 𝑋 ∈ 𝑉
umgrbi.y ⊢ 𝑌 ∈ 𝑉
umgrbi.n ⊢ 𝑋 ≠ 𝑌
Assertion umgrbi { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }

Proof

Step Hyp Ref Expression
1 umgrbi.x ⊢ 𝑋 ∈ 𝑉
2 umgrbi.y ⊢ 𝑌 ∈ 𝑉
3 umgrbi.n ⊢ 𝑋 ≠ 𝑌
4 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
5 1 2 4 mp2an ⊢ { 𝑋 , 𝑌 } ⊆ 𝑉
6 prex ⊢ { 𝑋 , 𝑌 } ∈ V
7 6 elpw ⊢ ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ↔ { 𝑋 , 𝑌 } ⊆ 𝑉 )
8 5 7 mpbir ⊢ { 𝑋 , 𝑌 } ∈ 𝒫 𝑉
9 hashprg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ≠ 𝑌 ↔ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 ) )
10 3 9 mpbii ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 )
11 1 2 10 mp2an ⊢ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2
12 fveqeq2 ⊢ ( 𝑥 = { 𝑋 , 𝑌 } → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 ) )
13 12 elrab ⊢ ( { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝑋 , 𝑌 } ) = 2 ) )
14 8 11 13 mpbir2an ⊢ { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }