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 )