Metamath Proof Explorer

Theorem fusgrfis

Description: A finite simple graph is of finite size, i.e. has a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018) (Revised by AV, 8-Nov-2020)

Ref Expression
Assertion fusgrfis 
|- ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ ( Vtx ` G ) e. Fin ) )
3 usgrop 
 |-  ( G e. USGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph )
4 fvex 
 |-  ( iEdg ` G ) e. _V
5 mptresid 
 |-  ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) = ( q e. { p e. ( Edg ` <. v , e >. ) | n e/ p } |-> q )
6 fvex 
 |-  ( Edg ` <. v , e >. ) e. _V
7 6 mptrabex 
 |-  ( q e. { p e. ( Edg ` <. v , e >. ) | n e/ p } |-> q ) e. _V
8 5 7 eqeltri 
 |-  ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) e. _V
9 eleq1 
 |-  ( e = ( iEdg ` G ) -> ( e e. Fin <-> ( iEdg ` G ) e. Fin ) )
10 9 adantl 
 |-  ( ( v = ( Vtx ` G ) /\ e = ( iEdg ` G ) ) -> ( e e. Fin <-> ( iEdg ` G ) e. Fin ) )
11 eleq1 
 |-  ( e = f -> ( e e. Fin <-> f e. Fin ) )
12 11 adantl 
 |-  ( ( v = w /\ e = f ) -> ( e e. Fin <-> f e. Fin ) )
13 vex 
 |-  v e. _V
14 vex 
 |-  e e. _V
15 13 14 opvtxfvi 
 |-  ( Vtx ` <. v , e >. ) = v
16 15 eqcomi 
 |-  v = ( Vtx ` <. v , e >. )
17 eqid 
 |-  ( Edg ` <. v , e >. ) = ( Edg ` <. v , e >. )
18 eqid 
 |-  { p e. ( Edg ` <. v , e >. ) | n e/ p } = { p e. ( Edg ` <. v , e >. ) | n e/ p }
19 eqid 
 |-  <. ( v \ { n } ) , ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) >. = <. ( v \ { n } ) , ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) >.
20 16 17 18 19 usgrres1 
 |-  ( ( <. v , e >. e. USGraph /\ n e. v ) -> <. ( v \ { n } ) , ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) >. e. USGraph )
21 eleq1 
 |-  ( f = ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) -> ( f e. Fin <-> ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) e. Fin ) )
22 21 adantl 
 |-  ( ( w = ( v \ { n } ) /\ f = ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) ) -> ( f e. Fin <-> ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) e. Fin ) )
23 13 14 pm3.2i 
 |-  ( v e. _V /\ e e. _V )
24 fusgrfisbase 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ <. v , e >. e. USGraph /\ ( # ` v ) = 0 ) -> e e. Fin )
25 23 24 mp3an1 
 |-  ( ( <. v , e >. e. USGraph /\ ( # ` v ) = 0 ) -> e e. Fin )
26 simpl 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) ) -> ( v e. _V /\ e e. _V ) )
27 simprr1 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) ) -> <. v , e >. e. USGraph )
28 eleq1 
 |-  ( ( # ` v ) = ( y + 1 ) -> ( ( # ` v ) e. NN0 <-> ( y + 1 ) e. NN0 ) )
29 hashclb 
 |-  ( v e. _V -> ( v e. Fin <-> ( # ` v ) e. NN0 ) )
30 29 biimprd 
 |-  ( v e. _V -> ( ( # ` v ) e. NN0 -> v e. Fin ) )
31 30 adantr 
 |-  ( ( v e. _V /\ e e. _V ) -> ( ( # ` v ) e. NN0 -> v e. Fin ) )
32 31 com12 
 |-  ( ( # ` v ) e. NN0 -> ( ( v e. _V /\ e e. _V ) -> v e. Fin ) )
33 28 32 syl6bir 
 |-  ( ( # ` v ) = ( y + 1 ) -> ( ( y + 1 ) e. NN0 -> ( ( v e. _V /\ e e. _V ) -> v e. Fin ) ) )
34 33 3ad2ant2 
 |-  ( ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) -> ( ( y + 1 ) e. NN0 -> ( ( v e. _V /\ e e. _V ) -> v e. Fin ) ) )
35 34 impcom 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( v e. _V /\ e e. _V ) -> v e. Fin ) )
36 35 impcom 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) ) -> v e. Fin )
37 opfusgr 
 |-  ( ( v e. _V /\ e e. _V ) -> ( <. v , e >. e. FinUSGraph <-> ( <. v , e >. e. USGraph /\ v e. Fin ) ) )
38 37 adantr 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) ) -> ( <. v , e >. e. FinUSGraph <-> ( <. v , e >. e. USGraph /\ v e. Fin ) ) )
39 27 36 38 mpbir2and 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) ) -> <. v , e >. e. FinUSGraph )
40 simprr3 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) ) -> n e. v )
41 26 39 40 3jca 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) ) -> ( ( v e. _V /\ e e. _V ) /\ <. v , e >. e. FinUSGraph /\ n e. v ) )
42 23 41 mpan 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( v e. _V /\ e e. _V ) /\ <. v , e >. e. FinUSGraph /\ n e. v ) )
43 fusgrfisstep 
 |-  ( ( ( v e. _V /\ e e. _V ) /\ <. v , e >. e. FinUSGraph /\ n e. v ) -> ( ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) e. Fin -> e e. Fin ) )
44 42 43 syl 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) e. Fin -> e e. Fin ) )
45 44 imp 
 |-  ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. USGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( _I |` { p e. ( Edg ` <. v , e >. ) | n e/ p } ) e. Fin ) -> e e. Fin )
46 4 8 10 12 20 22 25 45 opfi1ind 
 |-  ( ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. USGraph /\ ( Vtx ` G ) e. Fin ) -> ( iEdg ` G ) e. Fin )
47 3 46 sylan 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) e. Fin ) -> ( iEdg ` G ) e. Fin )
48 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
49 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
50 48 49 usgredgffibi 
 |-  ( G e. USGraph -> ( ( Edg ` G ) e. Fin <-> ( iEdg ` G ) e. Fin ) )
51 50 adantr 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) e. Fin ) -> ( ( Edg ` G ) e. Fin <-> ( iEdg ` G ) e. Fin ) )
52 47 51 mpbird 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) e. Fin ) -> ( Edg ` G ) e. Fin )
53 2 52 sylbi 
 |-  ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )