Theorem griedg0ssusgr

Description: The class of all simple graphs is a superclass of the class of empty graphs represented as ordered pairs. (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Hypothesis	griedg0prc.u	$$⊢U=\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}$$
Assertion	griedg0ssusgr	$$⊢U\subseteq \mathrm{USGraph}$$

Proof

Step	Hyp	Ref	Expression
1		griedg0prc.u	$$⊢U=\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}$$
2	1	eleq2i	$$⊢g\in U\leftrightarrow g\in \left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}$$
3		elopab	$$⊢g\in \left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\leftrightarrow \exists v\exists e\left(g=⟨v,e⟩\wedge e:\varnothing ⟶\varnothing \right)$$
4	2 3	bitri	$$⊢g\in U\leftrightarrow \exists v\exists e\left(g=⟨v,e⟩\wedge e:\varnothing ⟶\varnothing \right)$$
5		opex	$$⊢⟨v,e⟩\in \mathrm{V}$$
6	5	a1i	$$⊢e:\varnothing ⟶\varnothing \to ⟨v,e⟩\in \mathrm{V}$$
7		vex	$$⊢v\in \mathrm{V}$$
8		vex	$$⊢e\in \mathrm{V}$$
9	7 8	opiedgfvi	$$⊢\mathrm{iEdg}\left(⟨v,e⟩\right)=e$$
10		f0bi	$$⊢e:\varnothing ⟶\varnothing \leftrightarrow e=\varnothing$$
11	10	biimpi	$$⊢e:\varnothing ⟶\varnothing \to e=\varnothing$$
12	9 11	syl5eq	$$⊢e:\varnothing ⟶\varnothing \to \mathrm{iEdg}\left(⟨v,e⟩\right)=\varnothing$$
13	6 12	usgr0e	$$⊢e:\varnothing ⟶\varnothing \to ⟨v,e⟩\in \mathrm{USGraph}$$
14	13	adantl	$$⊢\left(g=⟨v,e⟩\wedge e:\varnothing ⟶\varnothing \right)\to ⟨v,e⟩\in \mathrm{USGraph}$$
15		eleq1	$$⊢g=⟨v,e⟩\to \left(g\in \mathrm{USGraph}\leftrightarrow ⟨v,e⟩\in \mathrm{USGraph}\right)$$
16	15	adantr	$$⊢\left(g=⟨v,e⟩\wedge e:\varnothing ⟶\varnothing \right)\to \left(g\in \mathrm{USGraph}\leftrightarrow ⟨v,e⟩\in \mathrm{USGraph}\right)$$
17	14 16	mpbird	$$⊢\left(g=⟨v,e⟩\wedge e:\varnothing ⟶\varnothing \right)\to g\in \mathrm{USGraph}$$
18	17	exlimivv	$$⊢\exists v\exists e\left(g=⟨v,e⟩\wedge e:\varnothing ⟶\varnothing \right)\to g\in \mathrm{USGraph}$$
19	4 18	sylbi	$$⊢g\in U\to g\in \mathrm{USGraph}$$
20	19	ssriv	$$⊢U\subseteq \mathrm{USGraph}$$