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

Metamath Proof Explorer

Theorem uhgr0vsize0

Description: The size of a hypergraph with no vertices (the null graph) is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 7-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		uhgr0v0e.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uhgr0v0e.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	uhgr0v0e	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = ∅ ) → 𝐸 = ∅ )
4	3	ex	⊢ ( 𝐺 ∈ UHGraph → ( 𝑉 = ∅ → 𝐸 = ∅ ) )
5	1	fvexi	⊢ 𝑉 ∈ V
6		hasheq0	⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 0 ↔ 𝑉 = ∅ ) )
7	5 6	ax-mp	⊢ ( ( ♯ ‘ 𝑉 ) = 0 ↔ 𝑉 = ∅ )
8	2	fvexi	⊢ 𝐸 ∈ V
9		hasheq0	⊢ ( 𝐸 ∈ V → ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ ) )
10	8 9	ax-mp	⊢ ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ )
11	4 7 10	3imtr4g	⊢ ( 𝐺 ∈ UHGraph → ( ( ♯ ‘ 𝑉 ) = 0 → ( ♯ ‘ 𝐸 ) = 0 ) )
12	11	imp	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ♯ ‘ 𝐸 ) = 0 )