Theorem isfusgrf1

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

	Ref	Expression
Hypotheses	isfusgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isfusgrf1.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	isfusgrf1	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ FinUSGraph ↔ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ 𝑉 ∈ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isfusgrf1.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3	1	isfusgr	⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
4	1 2	isusgrs	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ USGraph ↔ 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
5	4	anbi1d	⊢ ( 𝐺 ∈ 𝑊 → ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ↔ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ 𝑉 ∈ Fin ) ) )
6	3 5	syl5bb	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ FinUSGraph ↔ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ 𝑉 ∈ Fin ) ) )