Theorem uhgrstrrepe

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

	Ref	Expression
Hypotheses	uhgrstrrepe.v	$$⊢V={\mathrm{Base}}_G$$
	uhgrstrrepe.i	$$⊢I=\mathrm{ef}\left(\mathrm{ndx}\right)$$
	uhgrstrrepe.s	$$⊢\phi \to G\mathrm{Struct}X$$
	uhgrstrrepe.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}G$$
	uhgrstrrepe.w	$$⊢\phi \to E\in W$$
	uhgrstrrepe.e	$$⊢\phi \to E:\mathrm{dom}E⟶𝒫V\setminus \left\{\varnothing \right\}$$
Assertion	uhgrstrrepe	$$⊢\phi \to G\mathrm{sSet}⟨I,E⟩\in \mathrm{UHGraph}$$

Proof

Step	Hyp	Ref	Expression
1		uhgrstrrepe.v	$$⊢V={\mathrm{Base}}_G$$
2		uhgrstrrepe.i	$$⊢I=\mathrm{ef}\left(\mathrm{ndx}\right)$$
3		uhgrstrrepe.s	$$⊢\phi \to G\mathrm{Struct}X$$
4		uhgrstrrepe.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}G$$
5		uhgrstrrepe.w	$$⊢\phi \to E\in W$$
6		uhgrstrrepe.e	$$⊢\phi \to E:\mathrm{dom}E⟶𝒫V\setminus \left\{\varnothing \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	difeq1d	$$⊢\phi \to 𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}=𝒫V\setminus \left\{\varnothing \right\}$$
11	10	feq3d	$$⊢\phi \to \left(E:\mathrm{dom}E⟶𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}\leftrightarrow E:\mathrm{dom}E⟶𝒫V\setminus \left\{\varnothing \right\}\right)$$
12	6 11	mpbird	$$⊢\phi \to E:\mathrm{dom}E⟶𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}$$
13	2 3 4 5	setsiedg	$$⊢\phi \to \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)=E$$
14	13	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{dom}E$$
15	13 14	feq12d	$$⊢\phi \to \left(\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)⟶𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}\leftrightarrow E:\mathrm{dom}E⟶𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}\right)$$
16	12 15	mpbird	$$⊢\phi \to \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)⟶𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}$$
17		ovex	$$⊢G\mathrm{sSet}⟨I,E⟩\in \mathrm{V}$$
18		eqid	$$⊢\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)$$
19		eqid	$$⊢\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)=\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)$$
20	18 19	isuhgr	$$⊢G\mathrm{sSet}⟨I,E⟩\in \mathrm{V}\to \left(G\mathrm{sSet}⟨I,E⟩\in \mathrm{UHGraph}\leftrightarrow \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)⟶𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}\right)$$
21	17 20	mp1i	$$⊢\phi \to \left(G\mathrm{sSet}⟨I,E⟩\in \mathrm{UHGraph}\leftrightarrow \mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right):\mathrm{dom}\mathrm{iEdg}\left(G\mathrm{sSet}⟨I,E⟩\right)⟶𝒫\mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}\right)$$
22	16 21	mpbird	$$⊢\phi \to G\mathrm{sSet}⟨I,E⟩\in \mathrm{UHGraph}$$