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

Proof

Step Hyp Ref Expression
1 usgruhgr ⊢ V E ∈ USGraph → V E ∈ UHGraph
2 1 3ad2ant2 ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → V E ∈ UHGraph
3 opvtxfv ⊢ V ∈ X ∧ E ∈ Y → Vtx ⁡ V E = V
4 3 3ad2ant1 ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → Vtx ⁡ V E = 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 → V E ∈ USGraph → V = 0 → V = ∅
9 8 3imp ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → V = ∅
10 4 9 eqtrd ⊢ V ∈ X ∧ E ∈ Y ∧ V 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 ∈ UHGraph ∧ Vtx ⁡ V E = ∅ → Edg ⁡ V E = ∅
14 2 10 13 syl2anc ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → Edg ⁡ V E = ∅
15 0fi ⊢ ∅ ∈ Fin
16 14 15 eqeltrdi ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → Edg ⁡ V E ∈ Fin
17 eqid ⊢ iEdg ⁡ V E = iEdg ⁡ V E
18 17 12 usgredgffibi ⊢ V E ∈ USGraph → Edg ⁡ V E ∈ Fin ↔ iEdg ⁡ V E ∈ Fin
19 18 3ad2ant2 ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → Edg ⁡ V E ∈ Fin ↔ iEdg ⁡ V E ∈ Fin
20 opiedgfv ⊢ V ∈ X ∧ E ∈ Y → iEdg ⁡ V E = E
21 20 3ad2ant1 ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → iEdg ⁡ V E = E
22 21 eleq1d ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → iEdg ⁡ V E ∈ Fin ↔ E ∈ Fin
23 19 22 bitrd ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → Edg ⁡ V E ∈ Fin ↔ E ∈ Fin
24 16 23 mpbid ⊢ V ∈ X ∧ E ∈ Y ∧ V E ∈ USGraph ∧ V = 0 → E ∈ Fin