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

Metamath Proof Explorer

Theorem usgrexi

Description: An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 10-Nov-2021)

Ref Expression
Hypothesis usgrexi.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
Assertion usgrexi ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ USGraph )

Proof

Step Hyp Ref Expression
1 usgrexi.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 1 usgrexilem ⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
3 1 cusgrexilem1 ⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ 𝑃 ) ∈ V )
4 opiedgfv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃 ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( I ↾ 𝑃 ) )
5 3 4 mpdan ⊢ ( 𝑉 ∈ 𝑊 → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( I ↾ 𝑃 ) )
6 5 dmeqd ⊢ ( 𝑉 ∈ 𝑊 → dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = dom ( I ↾ 𝑃 ) )
7 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( I ↾ 𝑃 ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = 𝑉 )
8 3 7 mpdan ⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = 𝑉 )
9 8 pweqd ⊢ ( 𝑉 ∈ 𝑊 → 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = 𝒫 𝑉 )
10 9 rabeqdv ⊢ ( 𝑉 ∈ 𝑊 → { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
11 5 6 10 f1eq123d ⊢ ( 𝑉 ∈ 𝑊 → ( ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
12 2 11 mpbird ⊢ ( 𝑉 ∈ 𝑊 → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
13 opex ⊢ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ V
14 eqid ⊢ ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ )
15 eqid ⊢ ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ )
16 14 15 isusgrs ⊢ ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ V → ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ USGraph ↔ ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
17 13 16 mp1i ⊢ ( 𝑉 ∈ 𝑊 → ( ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ USGraph ↔ ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
18 12 17 mpbird ⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ( I ↾ 𝑃 ) ⟩ ∈ USGraph )