Theorem upgrfi

Description: An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

	Ref	Expression
Hypotheses	isupgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isupgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
Assertion	upgrfi	$$⊢\left(G\in \mathrm{UPGraph}\wedge EFnA\wedge F\in A\right)\to E\left(F\right)\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		isupgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isupgr.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
3	1 2	upgrle	$$⊢\left(G\in \mathrm{UPGraph}\wedge EFnA\wedge F\in A\right)\to \left|E\left(F\right)\right|\le 2$$
4		2re	$$⊢2\in ℝ$$
5		ltpnf	$$⊢2\in ℝ\to 2<\mathrm{+\infty }$$
6	4 5	ax-mp	$$⊢2<\mathrm{+\infty }$$
7	4	rexri	$$⊢2\in {ℝ}^{*}$$
8		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
9		xrltnle	$$⊢\left(2\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(2<\mathrm{+\infty }\leftrightarrow \neg \mathrm{+\infty }\le 2\right)$$
10	7 8 9	mp2an	$$⊢2<\mathrm{+\infty }\leftrightarrow \neg \mathrm{+\infty }\le 2$$
11	6 10	mpbi	$$⊢\neg \mathrm{+\infty }\le 2$$
12		fvex	$$⊢E\left(F\right)\in \mathrm{V}$$
13		hashinf	$$⊢\left(E\left(F\right)\in \mathrm{V}\wedge \neg E\left(F\right)\in \mathrm{Fin}\right)\to \left|E\left(F\right)\right|=\mathrm{+\infty }$$
14	12 13	mpan	$$⊢\neg E\left(F\right)\in \mathrm{Fin}\to \left|E\left(F\right)\right|=\mathrm{+\infty }$$
15	14	breq1d	$$⊢\neg E\left(F\right)\in \mathrm{Fin}\to \left(\left|E\left(F\right)\right|\le 2\leftrightarrow \mathrm{+\infty }\le 2\right)$$
16	11 15	mtbiri	$$⊢\neg E\left(F\right)\in \mathrm{Fin}\to \neg \left|E\left(F\right)\right|\le 2$$
17	16	con4i	$$⊢\left|E\left(F\right)\right|\le 2\to E\left(F\right)\in \mathrm{Fin}$$
18	3 17	syl	$$⊢\left(G\in \mathrm{UPGraph}\wedge EFnA\wedge F\in A\right)\to E\left(F\right)\in \mathrm{Fin}$$