Theorem 1hegrlfgr

Description: A graph G with one hyperedge joining at least two vertices is a loop-free graph. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Hypotheses	1hegrlfgr.a	$$⊢\phi \to A\in X$$
	1hegrlfgr.b	$$⊢\phi \to B\in V$$
	1hegrlfgr.c	$$⊢\phi \to C\in V$$
	1hegrlfgr.n	$$⊢\phi \to B\ne C$$
	1hegrlfgr.x	$$⊢\phi \to E\in 𝒫V$$
	1hegrlfgr.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,E⟩\right\}$$
	1hegrlfgr.e	$$⊢\phi \to \left\{B,C\right\}\subseteq E$$
Assertion	1hegrlfgr	$$⊢\phi \to \mathrm{iEdg}\left(G\right):\left\{A\right\}⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1hegrlfgr.a	$$⊢\phi \to A\in X$$
2		1hegrlfgr.b	$$⊢\phi \to B\in V$$
3		1hegrlfgr.c	$$⊢\phi \to C\in V$$
4		1hegrlfgr.n	$$⊢\phi \to B\ne C$$
5		1hegrlfgr.x	$$⊢\phi \to E\in 𝒫V$$
6		1hegrlfgr.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,E⟩\right\}$$
7		1hegrlfgr.e	$$⊢\phi \to \left\{B,C\right\}\subseteq E$$
8		f1osng	$$⊢\left(A\in X\wedge E\in 𝒫V\right)\to \left\{⟨A,E⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{E\right\}$$
9	1 5 8	syl2anc	$$⊢\phi \to \left\{⟨A,E⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{E\right\}$$
10		f1of	$$⊢\left\{⟨A,E⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{E\right\}\to \left\{⟨A,E⟩\right\}:\left\{A\right\}⟶\left\{E\right\}$$
11	9 10	syl	$$⊢\phi \to \left\{⟨A,E⟩\right\}:\left\{A\right\}⟶\left\{E\right\}$$
12		prid1g	$$⊢B\in V\to B\in \left\{B,C\right\}$$
13	2 12	syl	$$⊢\phi \to B\in \left\{B,C\right\}$$
14	7 13	sseldd	$$⊢\phi \to B\in E$$
15		prid2g	$$⊢C\in V\to C\in \left\{B,C\right\}$$
16	3 15	syl	$$⊢\phi \to C\in \left\{B,C\right\}$$
17	7 16	sseldd	$$⊢\phi \to C\in E$$
18	5 14 17 4	nehash2	$$⊢\phi \to 2\le \left|E\right|$$
19		fveq2	$$⊢x=E\to \left|x\right|=\left|E\right|$$
20	19	breq2d	$$⊢x=E\to \left(2\le \left|x\right|\leftrightarrow 2\le \left|E\right|\right)$$
21	20	elrab	$$⊢E\in \left\{x\in 𝒫V|2\le \left|x\right|\right\}\leftrightarrow \left(E\in 𝒫V\wedge 2\le \left|E\right|\right)$$
22	5 18 21	sylanbrc	$$⊢\phi \to E\in \left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
23	22	snssd	$$⊢\phi \to \left\{E\right\}\subseteq \left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
24	11 23	fssd	$$⊢\phi \to \left\{⟨A,E⟩\right\}:\left\{A\right\}⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
25	6	feq1d	$$⊢\phi \to \left(\mathrm{iEdg}\left(G\right):\left\{A\right\}⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}\leftrightarrow \left\{⟨A,E⟩\right\}:\left\{A\right\}⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}\right)$$
26	24 25	mpbird	$$⊢\phi \to \mathrm{iEdg}\left(G\right):\left\{A\right\}⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$