Metamath Proof Explorer

Theorem usgr1v0e

Description: The size of a (finite) simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 22-Oct-2020)

Ref Expression
Hypotheses fusgredgfi.v ⊢V=Vtx⁡G
fusgredgfi.e ⊢E=Edg⁡G
Assertion usgr1v0e ⊢G∈USGraph∧V=1→E=0

Proof

Step Hyp Ref Expression
1 fusgredgfi.v ⊢V=Vtx⁡G
2 fusgredgfi.e ⊢E=Edg⁡G
3 simpl ⊢G∈USGraph∧V=v→G∈USGraph
4 vex ⊢v∈V
5 1 eqeq1i ⊢V=v↔Vtx⁡G=v
6 5 biimpi ⊢V=v→Vtx⁡G=v
7 6 adantl ⊢G∈USGraph∧V=v→Vtx⁡G=v
8 usgr1vr ⊢v∈V∧Vtx⁡G=v→G∈USGraph→iEdg⁡G=∅
9 4 7 8 sylancr ⊢G∈USGraph∧V=v→G∈USGraph→iEdg⁡G=∅
10 3 9 mpd ⊢G∈USGraph∧V=v→iEdg⁡G=∅
11 2 eqeq1i ⊢E=∅↔Edg⁡G=∅
12 usgruhgr ⊢G∈USGraph→G∈UHGraph
13 uhgriedg0edg0 ⊢G∈UHGraph→Edg⁡G=∅↔iEdg⁡G=∅
14 12 13 syl ⊢G∈USGraph→Edg⁡G=∅↔iEdg⁡G=∅
15 14 adantr ⊢G∈USGraph∧V=v→Edg⁡G=∅↔iEdg⁡G=∅
16 11 15 bitrid ⊢G∈USGraph∧V=v→E=∅↔iEdg⁡G=∅
17 10 16 mpbird ⊢G∈USGraph∧V=v→E=∅
18 17 ex ⊢G∈USGraph→V=v→E=∅
19 18 exlimdv ⊢G∈USGraph→∃vV=v→E=∅
20 1 fvexi ⊢V∈V
21 hash1snb ⊢V∈V→V=1↔∃vV=v
22 20 21 mp1i ⊢G∈USGraph→V=1↔∃vV=v
23 2 fvexi ⊢E∈V
24 hasheq0 ⊢E∈V→E=0↔E=∅
25 23 24 mp1i ⊢G∈USGraph→E=0↔E=∅
26 19 22 25 3imtr4d ⊢G∈USGraph→V=1→E=0
27 26 imp ⊢G∈USGraph∧V=1→E=0