Description: An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | isubgrupgr.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| Assertion | isubgrusgr | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ USGraph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isubgrupgr.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | usgruhgr | ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph ) | |
| 3 | 1 | isubgrsubgr | ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 ) |
| 4 | 2 3 | sylan | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 ) |
| 5 | subusgr | ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 ) → ( 𝐺 ISubGr 𝑆 ) ∈ USGraph ) | |
| 6 | 4 5 | syldan | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ USGraph ) |