# 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 )