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=\left\{x\in 𝒫{\mathrm{Base}}_S|\left|x\right|=2\right\}$$
	structtousgr.s	$$⊢\phi \to S\mathrm{Struct}X$$
	structtousgr.g	$$⊢G=S\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_P⟩$$
	structtousgr.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}S$$
Assertion	structtousgr	$$⊢\phi \to G\in \mathrm{USGraph}$$

Proof

Step	Hyp	Ref	Expression
1		structtousgr.p	$$⊢P=\left\{x\in 𝒫{\mathrm{Base}}_S|\left|x\right|=2\right\}$$
2		structtousgr.s	$$⊢\phi \to S\mathrm{Struct}X$$
3		structtousgr.g	$$⊢G=S\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_P⟩$$
4		structtousgr.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}S$$
5		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
6		eqid	$$⊢\mathrm{ef}\left(\mathrm{ndx}\right)=\mathrm{ef}\left(\mathrm{ndx}\right)$$
7		fvex	$$⊢{\mathrm{Base}}_S\in \mathrm{V}$$
8	1	cusgrexilem1	$$⊢{\mathrm{Base}}_S\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_P\in \mathrm{V}$$
9	7 8	mp1i	$$⊢\phi \to {\mathrm{I}\upharpoonright }_P\in \mathrm{V}$$
10	1	usgrexilem	$$⊢{\mathrm{Base}}_S\in \mathrm{V}\to \left({\mathrm{I}\upharpoonright }_P\right):\mathrm{dom}\left({\mathrm{I}\upharpoonright }_P\right)\underset{1-1}{⟶}\left\{x\in 𝒫{\mathrm{Base}}_S|\left|x\right|=2\right\}$$
11	7 10	mp1i	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_P\right):\mathrm{dom}\left({\mathrm{I}\upharpoonright }_P\right)\underset{1-1}{⟶}\left\{x\in 𝒫{\mathrm{Base}}_S|\left|x\right|=2\right\}$$
12	5 6 2 4 9 11	usgrstrrepe	$$⊢\phi \to S\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_P⟩\in \mathrm{USGraph}$$
13	3 12	eqeltrid	$$⊢\phi \to G\in \mathrm{USGraph}$$