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