Theorem lfgredgge2

Description: An edge of a loop-free graph has at least two ends. (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	lfgredgge2	$$⊢\left(I:A⟶E\wedge X\in A\right)\to 2\le \left|I\left(X\right)\right|$$

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		eqid	$$⊢A=A$$
5	4 3	feq23i	$$⊢I:A⟶E\leftrightarrow I:A⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
6	5	biimpi	$$⊢I:A⟶E\to I:A⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
7	6	ffvelcdmda	$$⊢\left(I:A⟶E\wedge X\in A\right)\to I\left(X\right)\in \left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
8		fveq2	$$⊢y=I\left(X\right)\to \left|y\right|=\left|I\left(X\right)\right|$$
9	8	breq2d	$$⊢y=I\left(X\right)\to \left(2\le \left|y\right|\leftrightarrow 2\le \left|I\left(X\right)\right|\right)$$
10		fveq2	$$⊢x=y\to \left|x\right|=\left|y\right|$$
11	10	breq2d	$$⊢x=y\to \left(2\le \left|x\right|\leftrightarrow 2\le \left|y\right|\right)$$
12	11	cbvrabv	$$⊢\left\{x\in 𝒫V|2\le \left|x\right|\right\}=\left\{y\in 𝒫V|2\le \left|y\right|\right\}$$
13	9 12	elrab2	$$⊢I\left(X\right)\in \left\{x\in 𝒫V|2\le \left|x\right|\right\}\leftrightarrow \left(I\left(X\right)\in 𝒫V\wedge 2\le \left|I\left(X\right)\right|\right)$$
14	13	simprbi	$$⊢I\left(X\right)\in \left\{x\in 𝒫V|2\le \left|x\right|\right\}\to 2\le \left|I\left(X\right)\right|$$
15	7 14	syl	$$⊢\left(I:A⟶E\wedge X\in A\right)\to 2\le \left|I\left(X\right)\right|$$