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∈X∧E∈Y∧VE∈USGraph∧V=0→E∈Fin

Proof

Step Hyp Ref Expression
1 usgruhgr ⊢VE∈USGraph→VE∈UHGraph
2 1 3ad2ant2 ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→VE∈UHGraph
3 opvtxfv ⊢V∈X∧E∈Y→Vtx⁡VE=V
4 3 3ad2ant1 ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→Vtx⁡VE=V
5 hasheq0 ⊢V∈X→V=0↔V=∅
6 5 biimpd ⊢V∈X→V=0→V=∅
7 6 adantr ⊢V∈X∧E∈Y→V=0→V=∅
8 7 a1d ⊢V∈X∧E∈Y→VE∈USGraph→V=0→V=∅
9 8 3imp ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→V=∅
10 4 9 eqtrd ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→Vtx⁡VE=∅
11 eqid ⊢Vtx⁡VE=Vtx⁡VE
12 eqid ⊢Edg⁡VE=Edg⁡VE
13 11 12 uhgr0v0e ⊢VE∈UHGraph∧Vtx⁡VE=∅→Edg⁡VE=∅
14 2 10 13 syl2anc ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→Edg⁡VE=∅
15 0fin ⊢∅∈Fin
16 14 15 eqeltrdi ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→Edg⁡VE∈Fin
17 eqid ⊢iEdg⁡VE=iEdg⁡VE
18 17 12 usgredgffibi ⊢VE∈USGraph→Edg⁡VE∈Fin↔iEdg⁡VE∈Fin
19 18 3ad2ant2 ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→Edg⁡VE∈Fin↔iEdg⁡VE∈Fin
20 opiedgfv ⊢V∈X∧E∈Y→iEdg⁡VE=E
21 20 3ad2ant1 ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→iEdg⁡VE=E
22 21 eleq1d ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→iEdg⁡VE∈Fin↔E∈Fin
23 19 22 bitrd ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→Edg⁡VE∈Fin↔E∈Fin
24 16 23 mpbid ⊢V∈X∧E∈Y∧VE∈USGraph∧V=0→E∈Fin