Theorem lfgrnloop

Description: A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Hypotheses	lfuhgrnloopv.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	lfuhgrnloopv.a	$$⊢A=\mathrm{dom}I$$
	lfuhgrnloopv.e	$$⊢E=\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
Assertion	lfgrnloop	$$⊢I:A⟶E\to \left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		lfuhgrnloopv.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
2		lfuhgrnloopv.a	$$⊢A=\mathrm{dom}I$$
3		lfuhgrnloopv.e	$$⊢E=\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xI$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
6		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
7	3 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}xE$$
8	4 5 7	nff	$$⊢ℲxI:A⟶E$$
9		hashsn01	$$⊢\left(\left|\left\{U\right\}\right|=0\vee \left|\left\{U\right\}\right|=1\right)$$
10		2pos	$$⊢0<2$$
11		0re	$$⊢0\in ℝ$$
12		2re	$$⊢2\in ℝ$$
13	11 12	ltnlei	$$⊢0<2\leftrightarrow \neg 2\le 0$$
14	10 13	mpbi	$$⊢\neg 2\le 0$$
15		breq2	$$⊢\left|\left\{U\right\}\right|=0\to \left(2\le \left|\left\{U\right\}\right|\leftrightarrow 2\le 0\right)$$
16	14 15	mtbiri	$$⊢\left|\left\{U\right\}\right|=0\to \neg 2\le \left|\left\{U\right\}\right|$$
17		1lt2	$$⊢1<2$$
18		1re	$$⊢1\in ℝ$$
19	18 12	ltnlei	$$⊢1<2\leftrightarrow \neg 2\le 1$$
20	17 19	mpbi	$$⊢\neg 2\le 1$$
21		breq2	$$⊢\left|\left\{U\right\}\right|=1\to \left(2\le \left|\left\{U\right\}\right|\leftrightarrow 2\le 1\right)$$
22	20 21	mtbiri	$$⊢\left|\left\{U\right\}\right|=1\to \neg 2\le \left|\left\{U\right\}\right|$$
23	16 22	jaoi	$$⊢\left(\left|\left\{U\right\}\right|=0\vee \left|\left\{U\right\}\right|=1\right)\to \neg 2\le \left|\left\{U\right\}\right|$$
24	9 23	ax-mp	$$⊢\neg 2\le \left|\left\{U\right\}\right|$$
25		fveq2	$$⊢I\left(x\right)=\left\{U\right\}\to \left|I\left(x\right)\right|=\left|\left\{U\right\}\right|$$
26	25	breq2d	$$⊢I\left(x\right)=\left\{U\right\}\to \left(2\le \left|I\left(x\right)\right|\leftrightarrow 2\le \left|\left\{U\right\}\right|\right)$$
27	24 26	mtbiri	$$⊢I\left(x\right)=\left\{U\right\}\to \neg 2\le \left|I\left(x\right)\right|$$
28	1 2 3	lfgredgge2	$$⊢\left(I:A⟶E\wedge x\in A\right)\to 2\le \left|I\left(x\right)\right|$$
29	27 28	nsyl3	$$⊢\left(I:A⟶E\wedge x\in A\right)\to \neg I\left(x\right)=\left\{U\right\}$$
30	29	ex	$$⊢I:A⟶E\to \left(x\in A\to \neg I\left(x\right)=\left\{U\right\}\right)$$
31	8 30	ralrimi	$$⊢I:A⟶E\to \forall x\in A\neg I\left(x\right)=\left\{U\right\}$$
32		rabeq0	$$⊢\left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}=\varnothing \leftrightarrow \forall x\in A\neg I\left(x\right)=\left\{U\right\}$$
33	31 32	sylibr	$$⊢I:A⟶E\to \left\{x\in A|I\left(x\right)=\left\{U\right\}\right\}=\varnothing$$