This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )