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 e. ~P ( Base ` S ) | ( # ` x ) = 2 }
structtousgr.s 
|- ( ph -> S Struct X )
structtousgr.g 
|- G = ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )
structtousgr.b 
|- ( ph -> ( Base ` ndx ) e. dom S )
Assertion structtousgr 
|- ( ph -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 structtousgr.p 
 |-  P = { x e. ~P ( Base ` S ) | ( # ` x ) = 2 }
2 structtousgr.s 
 |-  ( ph -> S Struct X )
3 structtousgr.g 
 |-  G = ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )
4 structtousgr.b 
 |-  ( ph -> ( Base ` ndx ) e. dom S )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  ( .ef ` ndx ) = ( .ef ` ndx )
7 fvex 
 |-  ( Base ` S ) e. _V
8 1 cusgrexilem1 
 |-  ( ( Base ` S ) e. _V -> ( _I |` P ) e. _V )
9 7 8 mp1i 
 |-  ( ph -> ( _I |` P ) e. _V )
10 1 usgrexilem 
 |-  ( ( Base ` S ) e. _V -> ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P ( Base ` S ) | ( # ` x ) = 2 } )
11 7 10 mp1i 
 |-  ( ph -> ( _I |` P ) : dom ( _I |` P ) -1-1-> { x e. ~P ( Base ` S ) | ( # ` x ) = 2 } )
12 5 6 2 4 9 11 usgrstrrepe 
 |-  ( ph -> ( S sSet <. ( .ef ` ndx ) , ( _I |` P ) >. ) e. USGraph )
13 3 12 eqeltrid 
 |-  ( ph -> G e. USGraph )