This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgredgfi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion usgr1v0e ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝐸 ) = 0 )

Proof

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