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 e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) e. Fin )

Proof

Step Hyp Ref Expression
1 isupgr.v 
 |-  V = ( Vtx ` G )
2 isupgr.e 
 |-  E = ( iEdg ` G )
3 1 2 upgrle 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( # ` ( E ` F ) ) <_ 2 )
4 2re 
 |-  2 e. RR
5 ltpnf 
 |-  ( 2 e. RR -> 2 < +oo )
6 4 5 ax-mp 
 |-  2 < +oo
7 4 rexri 
 |-  2 e. RR*
8 pnfxr 
 |-  +oo e. RR*
9 xrltnle 
 |-  ( ( 2 e. RR* /\ +oo e. RR* ) -> ( 2 < +oo <-> -. +oo <_ 2 ) )
10 7 8 9 mp2an 
 |-  ( 2 < +oo <-> -. +oo <_ 2 )
11 6 10 mpbi 
 |-  -. +oo <_ 2
12 fvex 
 |-  ( E ` F ) e. _V
13 hashinf 
 |-  ( ( ( E ` F ) e. _V /\ -. ( E ` F ) e. Fin ) -> ( # ` ( E ` F ) ) = +oo )
14 12 13 mpan 
 |-  ( -. ( E ` F ) e. Fin -> ( # ` ( E ` F ) ) = +oo )
15 14 breq1d 
 |-  ( -. ( E ` F ) e. Fin -> ( ( # ` ( E ` F ) ) <_ 2 <-> +oo <_ 2 ) )
16 11 15 mtbiri 
 |-  ( -. ( E ` F ) e. Fin -> -. ( # ` ( E ` F ) ) <_ 2 )
17 16 con4i 
 |-  ( ( # ` ( E ` F ) ) <_ 2 -> ( E ` F ) e. Fin )
18 3 17 syl 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) e. Fin )