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 0fin 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