Theorem isushgr

Description: The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020) (Revised by AV, 9-Oct-2020)

	Ref	Expression
Hypotheses	isuhgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isuhgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
Assertion	isushgr	$$⊢G\in U\to \left(G\in \mathrm{USHGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}𝒫V\setminus \left\{\varnothing \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isuhgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isuhgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
3		df-ushgr	$$⊢\mathrm{USHGraph}=\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\right\}$$
4	3	eleq2i	$$⊢G\in \mathrm{USHGraph}\leftrightarrow G\in \left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\right\}$$
5		fveq2	$$⊢h=G\to \mathrm{iEdg}\left(h\right)=\mathrm{iEdg}\left(G\right)$$
6	5 2	eqtr4di	$$⊢h=G\to \mathrm{iEdg}\left(h\right)=E$$
7	5	dmeqd	$$⊢h=G\to \mathrm{dom}\mathrm{iEdg}\left(h\right)=\mathrm{dom}\mathrm{iEdg}\left(G\right)$$
8	2	eqcomi	$$⊢\mathrm{iEdg}\left(G\right)=E$$
9	8	dmeqi	$$⊢\mathrm{dom}\mathrm{iEdg}\left(G\right)=\mathrm{dom}E$$
10	7 9	eqtrdi	$$⊢h=G\to \mathrm{dom}\mathrm{iEdg}\left(h\right)=\mathrm{dom}E$$
11		fveq2	$$⊢h=G\to \mathrm{Vtx}\left(h\right)=\mathrm{Vtx}\left(G\right)$$
12	11 1	eqtr4di	$$⊢h=G\to \mathrm{Vtx}\left(h\right)=V$$
13	12	pweqd	$$⊢h=G\to 𝒫\mathrm{Vtx}\left(h\right)=𝒫V$$
14	13	difeq1d	$$⊢h=G\to 𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}=𝒫V\setminus \left\{\varnothing \right\}$$
15	6 10 14	f1eq123d	$$⊢h=G\to \left(\mathrm{iEdg}\left(h\right):\mathrm{dom}\mathrm{iEdg}\left(h\right)\underset{1-1}{⟶}𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}𝒫V\setminus \left\{\varnothing \right\}\right)$$
16		fvexd	$$⊢g=h\to \mathrm{Vtx}\left(g\right)\in \mathrm{V}$$
17		fveq2	$$⊢g=h\to \mathrm{Vtx}\left(g\right)=\mathrm{Vtx}\left(h\right)$$
18		fvexd	$$⊢\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\to \mathrm{iEdg}\left(g\right)\in \mathrm{V}$$
19		fveq2	$$⊢g=h\to \mathrm{iEdg}\left(g\right)=\mathrm{iEdg}\left(h\right)$$
20	19	adantr	$$⊢\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\to \mathrm{iEdg}\left(g\right)=\mathrm{iEdg}\left(h\right)$$
21		simpr	$$⊢\left(\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\wedge e=\mathrm{iEdg}\left(h\right)\right)\to e=\mathrm{iEdg}\left(h\right)$$
22	21	dmeqd	$$⊢\left(\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\wedge e=\mathrm{iEdg}\left(h\right)\right)\to \mathrm{dom}e=\mathrm{dom}\mathrm{iEdg}\left(h\right)$$
23		simpr	$$⊢\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\to v=\mathrm{Vtx}\left(h\right)$$
24	23	pweqd	$$⊢\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\to 𝒫v=𝒫\mathrm{Vtx}\left(h\right)$$
25	24	difeq1d	$$⊢\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\to 𝒫v\setminus \left\{\varnothing \right\}=𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}$$
26	25	adantr	$$⊢\left(\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\wedge e=\mathrm{iEdg}\left(h\right)\right)\to 𝒫v\setminus \left\{\varnothing \right\}=𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}$$
27	21 22 26	f1eq123d	$$⊢\left(\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\wedge e=\mathrm{iEdg}\left(h\right)\right)\to \left(e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\leftrightarrow \mathrm{iEdg}\left(h\right):\mathrm{dom}\mathrm{iEdg}\left(h\right)\underset{1-1}{⟶}𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}\right)$$
28	18 20 27	sbcied2	$$⊢\left(g=h\wedge v=\mathrm{Vtx}\left(h\right)\right)\to \left(\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\leftrightarrow \mathrm{iEdg}\left(h\right):\mathrm{dom}\mathrm{iEdg}\left(h\right)\underset{1-1}{⟶}𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}\right)$$
29	16 17 28	sbcied2	$$⊢g=h\to \left(\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\leftrightarrow \mathrm{iEdg}\left(h\right):\mathrm{dom}\mathrm{iEdg}\left(h\right)\underset{1-1}{⟶}𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}\right)$$
30	29	cbvabv	$$⊢\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\right\}=\left\{h|\mathrm{iEdg}\left(h\right):\mathrm{dom}\mathrm{iEdg}\left(h\right)\underset{1-1}{⟶}𝒫\mathrm{Vtx}\left(h\right)\setminus \left\{\varnothing \right\}\right\}$$
31	15 30	elab2g	$$⊢G\in U\to \left(G\in \left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\right\}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}𝒫V\setminus \left\{\varnothing \right\}\right)$$
32	4 31	syl5bb	$$⊢G\in U\to \left(G\in \mathrm{USHGraph}\leftrightarrow E:\mathrm{dom}E\underset{1-1}{⟶}𝒫V\setminus \left\{\varnothing \right\}\right)$$