Description: A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | finrusgrfusgr.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
Assertion | finrusgrfusgr | ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | finrusgrfusgr.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
2 | rusgrusgr | ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph ) | |
3 | 2 | anim1i | ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ) |
4 | 1 | isfusgr | ⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ) |
5 | 3 4 | sylibr | ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph ) |