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 ⊢ P = x ∈ 𝒫 Base S | x = 2
structtousgr.s ⊢ φ → S Struct X
structtousgr.g ⊢ G = S sSet ef ⁡ ndx I ↾ P
structtousgr.b ⊢ φ → Base ndx ∈ dom ⁡ S
Assertion structtousgr ⊢ φ → G ∈ USGraph

Proof

Step Hyp Ref Expression
1 structtousgr.p ⊢ P = x ∈ 𝒫 Base S | x = 2
2 structtousgr.s ⊢ φ → S Struct X
3 structtousgr.g ⊢ G = S sSet ef ⁡ ndx I ↾ P
4 structtousgr.b ⊢ φ → Base ndx ∈ dom ⁡ S
5 eqid ⊢ Base S = Base S
6 eqid ⊢ ef ⁡ ndx = ef ⁡ ndx
7 fvex ⊢ Base S ∈ V
8 1 cusgrexilem1 ⊢ Base S ∈ V → I ↾ P ∈ V
9 7 8 mp1i ⊢ φ → I ↾ P ∈ V
10 1 usgrexilem ⊢ Base S ∈ V → I ↾ P : dom ⁡ I ↾ P ⟶ 1-1 x ∈ 𝒫 Base S | x = 2
11 7 10 mp1i ⊢ φ → I ↾ P : dom ⁡ I ↾ P ⟶ 1-1 x ∈ 𝒫 Base S | x = 2
12 5 6 2 4 9 11 usgrstrrepe ⊢ φ → S sSet ef ⁡ ndx I ↾ P ∈ USGraph
13 3 12 eqeltrid ⊢ φ → G ∈ USGraph