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

Metamath Proof Explorer

Theorem uhgr0v0e

Description: The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020)

Ref Expression
Hypotheses uhgr0v0e.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgr0v0e.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion uhgr0v0e ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = ∅ ) → 𝐸 = ∅ )

Proof

Step Hyp Ref Expression
1 uhgr0v0e.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgr0v0e.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 eqeq1i ⊢ ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ )
4 uhgr0vb ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
5 4 biimpd ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )
6 5 ex ⊢ ( 𝐺 ∈ UHGraph → ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) = ∅ ) ) )
7 3 6 biimtrid ⊢ ( 𝐺 ∈ UHGraph → ( 𝑉 = ∅ → ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) = ∅ ) ) )
8 7 pm2.43a ⊢ ( 𝐺 ∈ UHGraph → ( 𝑉 = ∅ → ( iEdg ‘ 𝐺 ) = ∅ ) )
9 8 imp ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
10 2 eqeq1i ⊢ ( 𝐸 = ∅ ↔ ( Edg ‘ 𝐺 ) = ∅ )
11 uhgriedg0edg0 ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
12 10 11 bitrid ⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
13 12 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = ∅ ) → ( 𝐸 = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
14 9 13 mpbird ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = ∅ ) → 𝐸 = ∅ )