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 syl5bb ⊢ 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 → ∃ v V = v → E = ∅
20 1 fvexi ⊢ V ∈ V
21 hash1snb ⊢ V ∈ V → V = 1 ↔ ∃ v V = v
22 20 21 mp1i ⊢ G ∈ USGraph → V = 1 ↔ ∃ v V = 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