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

Metamath Proof Explorer

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 }