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

Metamath Proof Explorer

Theorem structtousgr

Description: Any (extensible) structure with a base set can be made a simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021) (Revised by AV, 17-Nov-2021)

Ref Expression
Hypotheses structtousgr.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
structtousgr.s ⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
structtousgr.g ⊢ 𝐺 = ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
structtousgr.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
Assertion structtousgr ( 𝜑 → 𝐺 ∈ USGraph )

Proof

Step Hyp Ref Expression
1 structtousgr.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 structtousgr.s ⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
3 structtousgr.g ⊢ 𝐺 = ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ )
4 structtousgr.b ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
5 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6 eqid ⊢ ( .ef ‘ ndx ) = ( .ef ‘ ndx )
7 fvex ⊢ ( Base ‘ 𝑆 ) ∈ V
8 1 cusgrexilem1 ⊢ ( ( Base ‘ 𝑆 ) ∈ V → ( I ↾ 𝑃 ) ∈ V )
9 7 8 mp1i ⊢ ( 𝜑 → ( I ↾ 𝑃 ) ∈ V )
10 1 usgrexilem ⊢ ( ( Base ‘ 𝑆 ) ∈ V → ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
11 7 10 mp1i ⊢ ( 𝜑 → ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 ( Base ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
12 5 6 2 4 9 11 usgrstrrepe ⊢ ( 𝜑 → ( 𝑆 sSet ⟨ ( .ef ‘ ndx ) , ( I ↾ 𝑃 ) ⟩ ) ∈ USGraph )
13 3 12 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ USGraph )