This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subumgr

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

Ref Expression
Assertion subumgr ( ( 𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ UMGraph )

Proof

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