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 }