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 }