Theorem isfusgrcl

Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020) (Revised by AV, 9-Jan-2020)

	Ref	Expression
Assertion	isfusgrcl	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) ∈ ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) )
3		fvex	⊢ ( Vtx ‘ 𝐺 ) ∈ V
4		hashclb	⊢ ( ( Vtx ‘ 𝐺 ) ∈ V → ( ( Vtx ‘ 𝐺 ) ∈ Fin ↔ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) ∈ ℕ0 ) )
5	3 4	mp1i	⊢ ( 𝐺 ∈ USGraph → ( ( Vtx ‘ 𝐺 ) ∈ Fin ↔ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) ∈ ℕ0 ) )
6	5	pm5.32i	⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) ↔ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) ∈ ℕ0 ) )
7	2 6	bitri	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) ∈ ℕ0 ) )