Metamath Proof Explorer

Theorem fusgrfisbase

Description: Induction base for fusgrfis . Main work is done in uhgr0v0e . (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 23-Oct-2020)

Ref Expression
Assertion fusgrfisbase 
|- ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> E e. Fin )

Proof

Step Hyp Ref Expression
1 usgruhgr 
 |-  ( <. V , E >. e. USGraph -> <. V , E >. e. UHGraph )
2 1 3ad2ant2 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> <. V , E >. e. UHGraph )
3 opvtxfv 
 |-  ( ( V e. X /\ E e. Y ) -> ( Vtx ` <. V , E >. ) = V )
4 3 3ad2ant1 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( Vtx ` <. V , E >. ) = V )
5 hasheq0 
 |-  ( V e. X -> ( ( # ` V ) = 0 <-> V = (/) ) )
6 5 biimpd 
 |-  ( V e. X -> ( ( # ` V ) = 0 -> V = (/) ) )
7 6 adantr 
 |-  ( ( V e. X /\ E e. Y ) -> ( ( # ` V ) = 0 -> V = (/) ) )
8 7 a1d 
 |-  ( ( V e. X /\ E e. Y ) -> ( <. V , E >. e. USGraph -> ( ( # ` V ) = 0 -> V = (/) ) ) )
9 8 3imp 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> V = (/) )
10 4 9 eqtrd 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( Vtx ` <. V , E >. ) = (/) )
11 eqid 
 |-  ( Vtx ` <. V , E >. ) = ( Vtx ` <. V , E >. )
12 eqid 
 |-  ( Edg ` <. V , E >. ) = ( Edg ` <. V , E >. )
13 11 12 uhgr0v0e 
 |-  ( ( <. V , E >. e. UHGraph /\ ( Vtx ` <. V , E >. ) = (/) ) -> ( Edg ` <. V , E >. ) = (/) )
14 2 10 13 syl2anc 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( Edg ` <. V , E >. ) = (/) )
15 0fi 
 |-  (/) e. Fin
16 14 15 eqeltrdi 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( Edg ` <. V , E >. ) e. Fin )
17 eqid 
 |-  ( iEdg ` <. V , E >. ) = ( iEdg ` <. V , E >. )
18 17 12 usgredgffibi 
 |-  ( <. V , E >. e. USGraph -> ( ( Edg ` <. V , E >. ) e. Fin <-> ( iEdg ` <. V , E >. ) e. Fin ) )
19 18 3ad2ant2 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( ( Edg ` <. V , E >. ) e. Fin <-> ( iEdg ` <. V , E >. ) e. Fin ) )
20 opiedgfv 
 |-  ( ( V e. X /\ E e. Y ) -> ( iEdg ` <. V , E >. ) = E )
21 20 3ad2ant1 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( iEdg ` <. V , E >. ) = E )
22 21 eleq1d 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( ( iEdg ` <. V , E >. ) e. Fin <-> E e. Fin ) )
23 19 22 bitrd 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> ( ( Edg ` <. V , E >. ) e. Fin <-> E e. Fin ) )
24 16 23 mpbid 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. USGraph /\ ( # ` V ) = 0 ) -> E e. Fin )