Metamath Proof Explorer

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 ⊢ V = Vtx ⁡ G
isfusgrf1.i ⊢ I = iEdg ⁡ G
Assertion isfusgrf1 ⊢ G ∈ W → G ∈ FinUSGraph ↔ I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 V | x = 2 ∧ V ∈ Fin

Proof

Step Hyp Ref Expression
1 isfusgr.v ⊢ V = Vtx ⁡ G
2 isfusgrf1.i ⊢ I = iEdg ⁡ G
3 1 isfusgr ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ Fin
4 1 2 isusgrs ⊢ G ∈ W → G ∈ USGraph ↔ I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 V | x = 2
5 4 anbi1d ⊢ G ∈ W → G ∈ USGraph ∧ V ∈ Fin ↔ I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 V | x = 2 ∧ V ∈ Fin
6 3 5 bitrid ⊢ G ∈ W → G ∈ FinUSGraph ↔ I : dom ⁡ I ⟶ 1-1 x ∈ 𝒫 V | x = 2 ∧ V ∈ Fin