Theorem isfusgr

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

	Ref	Expression
Hypothesis	isfusgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fveq2	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
3	2 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
4	3	eleq1d	⊢ ( 𝑔 = 𝐺 → ( ( Vtx ‘ 𝑔 ) ∈ Fin ↔ 𝑉 ∈ Fin ) )
5		df-fusgr	⊢ FinUSGraph = { 𝑔 ∈ USGraph ∣ ( Vtx ‘ 𝑔 ) ∈ Fin }
6	4 5	elrab2	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )