Metamath Proof Explorer

Theorem subumgr

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

Ref Expression
Assertion subumgr ⊢ G ∈ UMGraph ∧ S SubGraph G → S ∈ UMGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ S = Vtx ⁡ S
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 eqid ⊢ Edg ⁡ S = Edg ⁡ S
6 1 2 3 4 5 subgrprop2 ⊢ S SubGraph G → Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
7 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
8 subgruhgrfun ⊢ G ∈ UHGraph ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S
9 7 8 sylan ⊢ G ∈ UMGraph ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S
10 9 ancoms ⊢ S SubGraph G ∧ G ∈ UMGraph → Fun ⁡ iEdg ⁡ S
11 10 funfnd ⊢ S SubGraph G ∧ G ∈ UMGraph → iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S
12 11 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph → iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S
13 simplrl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → S SubGraph G
14 simplrr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → G ∈ UMGraph
15 simpr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ S
16 1 3 subumgredg2 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2
17 13 14 15 16 syl3anc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2
18 17 ralrimiva ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph → ∀ x ∈ dom ⁡ iEdg ⁡ S iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2
19 fnfvrnss ⊢ iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S ∧ ∀ x ∈ dom ⁡ iEdg ⁡ S iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2 → ran ⁡ iEdg ⁡ S ⊆ e ∈ 𝒫 Vtx ⁡ S | e = 2
20 12 18 19 syl2anc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph → ran ⁡ iEdg ⁡ S ⊆ e ∈ 𝒫 Vtx ⁡ S | e = 2
21 df-f ⊢ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2 ↔ iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S ∧ ran ⁡ iEdg ⁡ S ⊆ e ∈ 𝒫 Vtx ⁡ S | e = 2
22 12 20 21 sylanbrc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph → iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2
23 subgrv ⊢ S SubGraph G → S ∈ V ∧ G ∈ V
24 1 3 isumgrs ⊢ S ∈ V → S ∈ UMGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2
25 24 adantr ⊢ S ∈ V ∧ G ∈ V → S ∈ UMGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2
26 23 25 syl ⊢ S SubGraph G → S ∈ UMGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2
27 26 ad2antrl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph → S ∈ UMGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2
28 22 27 mpbird ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UMGraph → S ∈ UMGraph
29 28 ex ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → S SubGraph G ∧ G ∈ UMGraph → S ∈ UMGraph
30 6 29 syl ⊢ S SubGraph G → S SubGraph G ∧ G ∈ UMGraph → S ∈ UMGraph
31 30 anabsi8 ⊢ G ∈ UMGraph ∧ S SubGraph G → S ∈ UMGraph