# Metamath Proof Explorer

## Theorem uhgrspan1

Description: The induced subgraph S of a hypergraph G obtained by removing one vertex is actually a subgraph of G . A subgraph is called induced orspanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in Bollobas p. 2 and section 1.1 in Diestel p. 4). (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrspan1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
uhgrspan1.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
uhgrspan1.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{I}|{N}\notin {I}\left({i}\right)\right\}$
uhgrspan1.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩$
Assertion uhgrspan1 ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to {S}\mathrm{SubGraph}{G}$

### Proof

Step Hyp Ref Expression
1 uhgrspan1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 uhgrspan1.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 uhgrspan1.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{I}|{N}\notin {I}\left({i}\right)\right\}$
4 uhgrspan1.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩$
5 difssd ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to {V}\setminus \left\{{N}\right\}\subseteq {V}$
6 1 2 3 4 uhgrspan1lem3 ${⊢}\mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}}$
7 resresdm ${⊢}\mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}}\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({S}\right)}$
8 6 7 mp1i ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to \mathrm{iEdg}\left({S}\right)={{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({S}\right)}$
9 2 uhgrfun ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{Fun}{I}$
10 fvelima ${⊢}\left(\mathrm{Fun}{I}\wedge {c}\in {I}\left[{F}\right]\right)\to \exists {j}\in {F}\phantom{\rule{.4em}{0ex}}{I}\left({j}\right)={c}$
11 10 ex ${⊢}\mathrm{Fun}{I}\to \left({c}\in {I}\left[{F}\right]\to \exists {j}\in {F}\phantom{\rule{.4em}{0ex}}{I}\left({j}\right)={c}\right)$
12 9 11 syl ${⊢}{G}\in \mathrm{UHGraph}\to \left({c}\in {I}\left[{F}\right]\to \exists {j}\in {F}\phantom{\rule{.4em}{0ex}}{I}\left({j}\right)={c}\right)$
13 12 adantr ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to \left({c}\in {I}\left[{F}\right]\to \exists {j}\in {F}\phantom{\rule{.4em}{0ex}}{I}\left({j}\right)={c}\right)$
14 eqidd ${⊢}{i}={j}\to {N}={N}$
15 fveq2 ${⊢}{i}={j}\to {I}\left({i}\right)={I}\left({j}\right)$
16 14 15 neleq12d ${⊢}{i}={j}\to \left({N}\notin {I}\left({i}\right)↔{N}\notin {I}\left({j}\right)\right)$
17 16 3 elrab2 ${⊢}{j}\in {F}↔\left({j}\in \mathrm{dom}{I}\wedge {N}\notin {I}\left({j}\right)\right)$
18 fvexd ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\wedge \left({j}\in \mathrm{dom}{I}\wedge {N}\notin {I}\left({j}\right)\right)\right)\to {I}\left({j}\right)\in \mathrm{V}$
19 1 2 uhgrss ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {j}\in \mathrm{dom}{I}\right)\to {I}\left({j}\right)\subseteq {V}$
20 19 ad2ant2r ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\wedge \left({j}\in \mathrm{dom}{I}\wedge {N}\notin {I}\left({j}\right)\right)\right)\to {I}\left({j}\right)\subseteq {V}$
21 simprr ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\wedge \left({j}\in \mathrm{dom}{I}\wedge {N}\notin {I}\left({j}\right)\right)\right)\to {N}\notin {I}\left({j}\right)$
22 elpwdifsn ${⊢}\left({I}\left({j}\right)\in \mathrm{V}\wedge {I}\left({j}\right)\subseteq {V}\wedge {N}\notin {I}\left({j}\right)\right)\to {I}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)$
23 18 20 21 22 syl3anc ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\wedge \left({j}\in \mathrm{dom}{I}\wedge {N}\notin {I}\left({j}\right)\right)\right)\to {I}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)$
24 eleq1 ${⊢}{c}={I}\left({j}\right)\to \left({c}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)↔{I}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
25 24 eqcoms ${⊢}{I}\left({j}\right)={c}\to \left({c}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)↔{I}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
26 23 25 syl5ibrcom ${⊢}\left(\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\wedge \left({j}\in \mathrm{dom}{I}\wedge {N}\notin {I}\left({j}\right)\right)\right)\to \left({I}\left({j}\right)={c}\to {c}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
27 26 ex ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to \left(\left({j}\in \mathrm{dom}{I}\wedge {N}\notin {I}\left({j}\right)\right)\to \left({I}\left({j}\right)={c}\to {c}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)\right)$
28 17 27 syl5bi ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to \left({j}\in {F}\to \left({I}\left({j}\right)={c}\to {c}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)\right)$
29 28 rexlimdv ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to \left(\exists {j}\in {F}\phantom{\rule{.4em}{0ex}}{I}\left({j}\right)={c}\to {c}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
30 13 29 syld ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to \left({c}\in {I}\left[{F}\right]\to {c}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
31 30 ssrdv ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to {I}\left[{F}\right]\subseteq 𝒫\left({V}\setminus \left\{{N}\right\}\right)$
32 opex ${⊢}⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩\in \mathrm{V}$
33 4 32 eqeltri ${⊢}{S}\in \mathrm{V}$
34 33 a1i ${⊢}{N}\in {V}\to {S}\in \mathrm{V}$
35 1 2 3 4 uhgrspan1lem2 ${⊢}\mathrm{Vtx}\left({S}\right)={V}\setminus \left\{{N}\right\}$
36 35 eqcomi ${⊢}{V}\setminus \left\{{N}\right\}=\mathrm{Vtx}\left({S}\right)$
37 eqid ${⊢}\mathrm{iEdg}\left({S}\right)=\mathrm{iEdg}\left({S}\right)$
38 6 rneqi ${⊢}\mathrm{ran}\mathrm{iEdg}\left({S}\right)=\mathrm{ran}\left({{I}↾}_{{F}}\right)$
39 edgval ${⊢}\mathrm{Edg}\left({S}\right)=\mathrm{ran}\mathrm{iEdg}\left({S}\right)$
40 df-ima ${⊢}{I}\left[{F}\right]=\mathrm{ran}\left({{I}↾}_{{F}}\right)$
41 38 39 40 3eqtr4ri ${⊢}{I}\left[{F}\right]=\mathrm{Edg}\left({S}\right)$
42 36 1 37 2 41 issubgr ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {S}\in \mathrm{V}\right)\to \left({S}\mathrm{SubGraph}{G}↔\left({V}\setminus \left\{{N}\right\}\subseteq {V}\wedge \mathrm{iEdg}\left({S}\right)={{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({S}\right)}\wedge {I}\left[{F}\right]\subseteq 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)\right)$
43 34 42 sylan2 ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to \left({S}\mathrm{SubGraph}{G}↔\left({V}\setminus \left\{{N}\right\}\subseteq {V}\wedge \mathrm{iEdg}\left({S}\right)={{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({S}\right)}\wedge {I}\left[{F}\right]\subseteq 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)\right)$
44 5 8 31 43 mpbir3and ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {N}\in {V}\right)\to {S}\mathrm{SubGraph}{G}$