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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isupgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	upgrfi	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		isupgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isupgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3	1 2	upgrle	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ 2 )
4		2re	⊢ 2 ∈ ℝ
5		ltpnf	⊢ ( 2 ∈ ℝ → 2 < +∞ )
6	4 5	ax-mp	⊢ 2 < +∞
7	4	rexri	⊢ 2 ∈ ℝ*
8		pnfxr	⊢ +∞ ∈ ℝ*
9		xrltnle	⊢ ( ( 2 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 2 < +∞ ↔ ¬ +∞ ≤ 2 ) )
10	7 8 9	mp2an	⊢ ( 2 < +∞ ↔ ¬ +∞ ≤ 2 )
11	6 10	mpbi	⊢ ¬ +∞ ≤ 2
12		fvex	⊢ ( 𝐸 ‘ 𝐹 ) ∈ V
13		hashinf	⊢ ( ( ( 𝐸 ‘ 𝐹 ) ∈ V ∧ ¬ ( 𝐸 ‘ 𝐹 ) ∈ Fin ) → ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) = +∞ )
14	12 13	mpan	⊢ ( ¬ ( 𝐸 ‘ 𝐹 ) ∈ Fin → ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) = +∞ )
15	14	breq1d	⊢ ( ¬ ( 𝐸 ‘ 𝐹 ) ∈ Fin → ( ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ 2 ↔ +∞ ≤ 2 ) )
16	11 15	mtbiri	⊢ ( ¬ ( 𝐸 ‘ 𝐹 ) ∈ Fin → ¬ ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ 2 )
17	16	con4i	⊢ ( ( ♯ ‘ ( 𝐸 ‘ 𝐹 ) ) ≤ 2 → ( 𝐸 ‘ 𝐹 ) ∈ Fin )
18	3 17	syl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ∈ Fin )