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 bilani ⊢ G ∈ USGraph ∧ V = v → Vtx ⁡ G = v
7 usgr1vr ⊢ v ∈ V ∧ Vtx ⁡ G = v → G ∈ USGraph → iEdg ⁡ G = ∅
8 4 6 7 sylancr ⊢ G ∈ USGraph ∧ V = v → G ∈ USGraph → iEdg ⁡ G = ∅
9 3 8 mpd ⊢ G ∈ USGraph ∧ V = v → iEdg ⁡ G = ∅
10 2 eqeq1i ⊢ E = ∅ ↔ Edg ⁡ G = ∅
11 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
12 uhgriedg0edg0 ⊢ G ∈ UHGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
13 11 12 syl ⊢ G ∈ USGraph → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
14 13 adantr ⊢ G ∈ USGraph ∧ V = v → Edg ⁡ G = ∅ ↔ iEdg ⁡ G = ∅
15 10 14 bitrid ⊢ G ∈ USGraph ∧ V = v → E = ∅ ↔ iEdg ⁡ G = ∅
16 9 15 mpbird ⊢ G ∈ USGraph ∧ V = v → E = ∅
17 16 ex ⊢ G ∈ USGraph → V = v → E = ∅
18 17 exlimdv ⊢ G ∈ USGraph → ∃ v V = v → E = ∅
19 1 fvexi ⊢ V ∈ V
20 hash1snb ⊢ V ∈ V → V = 1 ↔ ∃ v V = v
21 19 20 mp1i ⊢ G ∈ USGraph → V = 1 ↔ ∃ v V = v
22 2 fvexi ⊢ E ∈ V
23 hasheq0 ⊢ E ∈ V → E = 0 ↔ E = ∅
24 22 23 mp1i ⊢ G ∈ USGraph → E = 0 ↔ E = ∅
25 18 21 24 3imtr4d ⊢ G ∈ USGraph → V = 1 → E = 0
26 25 imp ⊢ G ∈ USGraph ∧ V = 1 → E = 0