Theorem usgr1e

Description: A simple graph with one edge (with additional assumption that B =/= C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 18-Oct-2020)

	Ref	Expression
Hypotheses	uspgr1e.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	uspgr1e.a	$$⊢\phi \to A\in X$$
	uspgr1e.b	$$⊢\phi \to B\in V$$
	uspgr1e.c	$$⊢\phi \to C\in V$$
	uspgr1e.e	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{B,C\right\}⟩\right\}$$
	usgr1e.e	$$⊢\phi \to B\ne C$$
Assertion	usgr1e	$$⊢\phi \to G\in \mathrm{USGraph}$$

Proof

Step	Hyp	Ref	Expression
1		uspgr1e.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		uspgr1e.a	$$⊢\phi \to A\in X$$
3		uspgr1e.b	$$⊢\phi \to B\in V$$
4		uspgr1e.c	$$⊢\phi \to C\in V$$
5		uspgr1e.e	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{B,C\right\}⟩\right\}$$
6		usgr1e.e	$$⊢\phi \to B\ne C$$
7	1 2 3 4 5	uspgr1e	$$⊢\phi \to G\in \mathrm{USHGraph}$$
8		hashprg	$$⊢\left(B\in V\wedge C\in V\right)\to \left(B\ne C\leftrightarrow \left|\left\{B,C\right\}\right|=2\right)$$
9	3 4 8	syl2anc	$$⊢\phi \to \left(B\ne C\leftrightarrow \left|\left\{B,C\right\}\right|=2\right)$$
10	6 9	mpbid	$$⊢\phi \to \left|\left\{B,C\right\}\right|=2$$
11		prex	$$⊢\left\{B,C\right\}\in \mathrm{V}$$
12		fveqeq2	$$⊢x=\left\{B,C\right\}\to \left(\left|x\right|=2\leftrightarrow \left|\left\{B,C\right\}\right|=2\right)$$
13	11 12	ralsn	$$⊢\forall x\in \left\{\left\{B,C\right\}\right\}\left|x\right|=2\leftrightarrow \left|\left\{B,C\right\}\right|=2$$
14	10 13	sylibr	$$⊢\phi \to \forall x\in \left\{\left\{B,C\right\}\right\}\left|x\right|=2$$
15		edgval	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
16	15	a1i	$$⊢\phi \to \mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
17	5	rneqd	$$⊢\phi \to \mathrm{ran}\mathrm{iEdg}\left(G\right)=\mathrm{ran}\left\{⟨A,\left\{B,C\right\}⟩\right\}$$
18		rnsnopg	$$⊢A\in X\to \mathrm{ran}\left\{⟨A,\left\{B,C\right\}⟩\right\}=\left\{\left\{B,C\right\}\right\}$$
19	2 18	syl	$$⊢\phi \to \mathrm{ran}\left\{⟨A,\left\{B,C\right\}⟩\right\}=\left\{\left\{B,C\right\}\right\}$$
20	16 17 19	3eqtrd	$$⊢\phi \to \mathrm{Edg}\left(G\right)=\left\{\left\{B,C\right\}\right\}$$
21	20	raleqdv	$$⊢\phi \to \left(\forall x\in \mathrm{Edg}\left(G\right)\left|x\right|=2\leftrightarrow \forall x\in \left\{\left\{B,C\right\}\right\}\left|x\right|=2\right)$$
22	14 21	mpbird	$$⊢\phi \to \forall x\in \mathrm{Edg}\left(G\right)\left|x\right|=2$$
23		usgruspgrb	$$⊢G\in \mathrm{USGraph}\leftrightarrow \left(G\in \mathrm{USHGraph}\wedge \forall x\in \mathrm{Edg}\left(G\right)\left|x\right|=2\right)$$
24	7 22 23	sylanbrc	$$⊢\phi \to G\in \mathrm{USGraph}$$