# Metamath Proof Explorer

## Theorem subumgr

Description: A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020)

Ref Expression
Assertion subumgr ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {S}\mathrm{SubGraph}{G}\right)\to {S}\in \mathrm{UMGraph}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({S}\right)=\mathrm{Vtx}\left({S}\right)$
2 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
3 eqid ${⊢}\mathrm{iEdg}\left({S}\right)=\mathrm{iEdg}\left({S}\right)$
4 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
5 eqid ${⊢}\mathrm{Edg}\left({S}\right)=\mathrm{Edg}\left({S}\right)$
6 1 2 3 4 5 subgrprop2 ${⊢}{S}\mathrm{SubGraph}{G}\to \left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)$
7 umgruhgr ${⊢}{G}\in \mathrm{UMGraph}\to {G}\in \mathrm{UHGraph}$
8 subgruhgrfun ${⊢}\left({G}\in \mathrm{UHGraph}\wedge {S}\mathrm{SubGraph}{G}\right)\to \mathrm{Fun}\mathrm{iEdg}\left({S}\right)$
9 7 8 sylan ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {S}\mathrm{SubGraph}{G}\right)\to \mathrm{Fun}\mathrm{iEdg}\left({S}\right)$
10 9 ancoms ${⊢}\left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\to \mathrm{Fun}\mathrm{iEdg}\left({S}\right)$
11 10 funfnd ${⊢}\left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\to \mathrm{iEdg}\left({S}\right)Fn\mathrm{dom}\mathrm{iEdg}\left({S}\right)$
12 11 adantl ${⊢}\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\to \mathrm{iEdg}\left({S}\right)Fn\mathrm{dom}\mathrm{iEdg}\left({S}\right)$
13 simplrl ${⊢}\left(\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\wedge {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)\right)\to {S}\mathrm{SubGraph}{G}$
14 simplrr ${⊢}\left(\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\wedge {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)\right)\to {G}\in \mathrm{UMGraph}$
15 simpr ${⊢}\left(\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\wedge {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)\right)\to {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)$
16 1 3 subumgredg2 ${⊢}\left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\wedge {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)\right)\to \mathrm{iEdg}\left({S}\right)\left({x}\right)\in \left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}$
17 13 14 15 16 syl3anc ${⊢}\left(\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\wedge {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)\right)\to \mathrm{iEdg}\left({S}\right)\left({x}\right)\in \left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}$
18 17 ralrimiva ${⊢}\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\to \forall {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({S}\right)\left({x}\right)\in \left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}$
19 fnfvrnss ${⊢}\left(\mathrm{iEdg}\left({S}\right)Fn\mathrm{dom}\mathrm{iEdg}\left({S}\right)\wedge \forall {x}\in \mathrm{dom}\mathrm{iEdg}\left({S}\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({S}\right)\left({x}\right)\in \left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}\right)\to \mathrm{ran}\mathrm{iEdg}\left({S}\right)\subseteq \left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}$
20 12 18 19 syl2anc ${⊢}\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\to \mathrm{ran}\mathrm{iEdg}\left({S}\right)\subseteq \left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}$
21 df-f ${⊢}\mathrm{iEdg}\left({S}\right):\mathrm{dom}\mathrm{iEdg}\left({S}\right)⟶\left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}↔\left(\mathrm{iEdg}\left({S}\right)Fn\mathrm{dom}\mathrm{iEdg}\left({S}\right)\wedge \mathrm{ran}\mathrm{iEdg}\left({S}\right)\subseteq \left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}\right)$
22 12 20 21 sylanbrc ${⊢}\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\to \mathrm{iEdg}\left({S}\right):\mathrm{dom}\mathrm{iEdg}\left({S}\right)⟶\left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}$
23 subgrv ${⊢}{S}\mathrm{SubGraph}{G}\to \left({S}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)$
24 1 3 isumgrs ${⊢}{S}\in \mathrm{V}\to \left({S}\in \mathrm{UMGraph}↔\mathrm{iEdg}\left({S}\right):\mathrm{dom}\mathrm{iEdg}\left({S}\right)⟶\left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}\right)$
25 24 adantr ${⊢}\left({S}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\to \left({S}\in \mathrm{UMGraph}↔\mathrm{iEdg}\left({S}\right):\mathrm{dom}\mathrm{iEdg}\left({S}\right)⟶\left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}\right)$
26 23 25 syl ${⊢}{S}\mathrm{SubGraph}{G}\to \left({S}\in \mathrm{UMGraph}↔\mathrm{iEdg}\left({S}\right):\mathrm{dom}\mathrm{iEdg}\left({S}\right)⟶\left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}\right)$
27 26 ad2antrl ${⊢}\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\to \left({S}\in \mathrm{UMGraph}↔\mathrm{iEdg}\left({S}\right):\mathrm{dom}\mathrm{iEdg}\left({S}\right)⟶\left\{{e}\in 𝒫\mathrm{Vtx}\left({S}\right)|\left|{e}\right|=2\right\}\right)$
28 22 27 mpbird ${⊢}\left(\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\wedge \left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\right)\to {S}\in \mathrm{UMGraph}$
29 28 ex ${⊢}\left(\mathrm{Vtx}\left({S}\right)\subseteq \mathrm{Vtx}\left({G}\right)\wedge \mathrm{iEdg}\left({S}\right)\subseteq \mathrm{iEdg}\left({G}\right)\wedge \mathrm{Edg}\left({S}\right)\subseteq 𝒫\mathrm{Vtx}\left({S}\right)\right)\to \left(\left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\to {S}\in \mathrm{UMGraph}\right)$
30 6 29 syl ${⊢}{S}\mathrm{SubGraph}{G}\to \left(\left({S}\mathrm{SubGraph}{G}\wedge {G}\in \mathrm{UMGraph}\right)\to {S}\in \mathrm{UMGraph}\right)$
31 30 anabsi8 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {S}\mathrm{SubGraph}{G}\right)\to {S}\in \mathrm{UMGraph}$