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 ⊢ V = Vtx ⁡ G
isupgr.e ⊢ E = iEdg ⁡ G
Assertion upgrfi ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ Fin

Proof

Step Hyp Ref Expression
1 isupgr.v ⊢ V = Vtx ⁡ G
2 isupgr.e ⊢ E = iEdg ⁡ G
3 1 2 upgrle ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ≤ 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 ⊢ E ⁡ F ∈ V
13 hashinf ⊢ E ⁡ F ∈ V ∧ ¬ E ⁡ F ∈ Fin → E ⁡ F = +∞
14 12 13 mpan ⊢ ¬ E ⁡ F ∈ Fin → E ⁡ F = +∞
15 14 breq1d ⊢ ¬ E ⁡ F ∈ Fin → E ⁡ F ≤ 2 ↔ +∞ ≤ 2
16 11 15 mtbiri ⊢ ¬ E ⁡ F ∈ Fin → ¬ E ⁡ F ≤ 2
17 16 con4i ⊢ E ⁡ F ≤ 2 → E ⁡ F ∈ Fin
18 3 17 syl ⊢ G ∈ UPGraph ∧ E Fn A ∧ F ∈ A → E ⁡ F ∈ Fin