Theorem usgrstrrepe

Description: Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring ( ph -> G Struct X ) , it would be sufficient to require ( ph -> Fun ( G \ { (/) } ) ) and ( ph -> G e. _V ) . (Contributed by AV, 13-Nov-2021) (Proof shortened by AV, 16-Nov-2021)

	Ref	Expression
Hypotheses	usgrstrrepe.v	$$⊢V={\mathrm{Base}}_G$$
	usgrstrrepe.i	$$⊢I=\mathrm{ef}\left(\mathrm{ndx}\right)$$
	usgrstrrepe.s	$$⊢\phi \to G\mathrm{Struct}X$$
	usgrstrrepe.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}G$$
	usgrstrrepe.w	$$⊢\phi \to E\in W$$
	usgrstrrepe.e	$$⊢\phi \to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
Assertion	usgrstrrepe	$$⊢\phi \to G\mathrm{sSet}⟨I,E⟩\in \mathrm{USGraph}$$

Proof

Step	Hyp	Ref	Expression
1		usgrstrrepe.v	$$⊢V={\mathrm{Base}}_G$$
2		usgrstrrepe.i	$$⊢I=\mathrm{ef}\left(\mathrm{ndx}\right)$$
3		usgrstrrepe.s	$$⊢\phi \to G\mathrm{Struct}X$$
4		usgrstrrepe.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}G$$
5		usgrstrrepe.w	$$⊢\phi \to E\in W$$
6		usgrstrrepe.e	$$⊢\phi \to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
7	2 3 4 5	setsvtx	$$⊢\phi \to \mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)={\mathrm{Base}}_G$$
8	7 1	eqtr4di	$$⊢\phi \to \mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)=V$$
9	8	pweqd	$$⊢\phi \to 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)=𝒫V$$
10	9	rabeqdv	$$⊢\phi \to \left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
11		f1eq3	$$⊢\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}\to \left(E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
12	10 11	syl	$$⊢\phi \to \left(E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
13	6 12	mpbird	$$⊢\phi \to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}$$
14	2 3 4 5	setsiedg	$$⊢\phi \to \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)=E$$
15	14	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{dom}E$$
16		eqidd	$$⊢\phi \to \left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}=\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}$$
17	14 15 16	f1eq123d	$$⊢\phi \to \left(\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}\right)$$
18	13 17	mpbird	$$⊢\phi \to \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}$$
19		ovex	$$⊢G\mathrm{sSet}⟨I,E⟩\in \mathrm{V}$$
20		eqid	$$⊢\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)$$
21		eqid	$$⊢\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)$$
22	20 21	isusgrs	$$⊢G\mathrm{sSet}⟨I,E⟩\in \mathrm{V}\to \left(G\mathrm{sSet}⟨I,E⟩\in \mathrm{USGraph}\leftrightarrow \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}\right)$$
23	19 22	mp1i	$$⊢\phi \to \left(G\mathrm{sSet}⟨I,E⟩\in \mathrm{USGraph}\leftrightarrow \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)\underset{1-1}{⟶}\left\{x\in 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)|\left|x\right|=2\right\}\right)$$
24	18 23	mpbird	$$⊢\phi \to G\mathrm{sSet}⟨I,E⟩\in \mathrm{USGraph}$$