Theorem upgrbi

Description: Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 28-Feb-2021)

	Ref	Expression
Hypotheses	upgrbi.x	⊢ 𝑋 ∈ 𝑉
	upgrbi.y	⊢ 𝑌 ∈ 𝑉
Assertion	upgrbi	⊢ { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }

Proof

Step	Hyp	Ref	Expression
1		upgrbi.x	⊢ 𝑋 ∈ 𝑉
2		upgrbi.y	⊢ 𝑌 ∈ 𝑉
3		prssi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
4	1 2 3	mp2an	⊢ { 𝑋 , 𝑌 } ⊆ 𝑉
5		prex	⊢ { 𝑋 , 𝑌 } ∈ V
6	5	elpw	⊢ ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ↔ { 𝑋 , 𝑌 } ⊆ 𝑉 )
7	4 6	mpbir	⊢ { 𝑋 , 𝑌 } ∈ 𝒫 𝑉
8	1	elexi	⊢ 𝑋 ∈ V
9	8	prnz	⊢ { 𝑋 , 𝑌 } ≠ ∅
10		eldifsn	⊢ ( { 𝑋 , 𝑌 } ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ∧ { 𝑋 , 𝑌 } ≠ ∅ ) )
11	7 9 10	mpbir2an	⊢ { 𝑋 , 𝑌 } ∈ ( 𝒫 𝑉 ∖ { ∅ } )
12		hashprlei	⊢ ( { 𝑋 , 𝑌 } ∈ Fin ∧ ( ♯ ‘ { 𝑋 , 𝑌 } ) ≤ 2 )
13	12	simpri	⊢ ( ♯ ‘ { 𝑋 , 𝑌 } ) ≤ 2
14		fveq2	⊢ ( 𝑥 = { 𝑋 , 𝑌 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑋 , 𝑌 } ) )
15	14	breq1d	⊢ ( 𝑥 = { 𝑋 , 𝑌 } → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ ( ♯ ‘ { 𝑋 , 𝑌 } ) ≤ 2 ) )
16	15	elrab	⊢ ( { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ ( { 𝑋 , 𝑌 } ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ { 𝑋 , 𝑌 } ) ≤ 2 ) )
17	11 13 16	mpbir2an	⊢ { 𝑋 , 𝑌 } ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }