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

Metamath Proof Explorer

Theorem subgrprop3

Description: The properties of a subgraph: If S is a subgraph of G , its vertices are also vertices of G , and its edges are also edges of G . (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses subgrprop3.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
subgrprop3.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
subgrprop3.e ⊢ 𝐸 = ( Edg ‘ 𝑆 )
subgrprop3.b ⊢ 𝐵 = ( Edg ‘ 𝐺 )
Assertion subgrprop3 ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subgrprop3.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
2 subgrprop3.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
3 subgrprop3.e ⊢ 𝐸 = ( Edg ‘ 𝑆 )
4 subgrprop3.b ⊢ 𝐵 = ( Edg ‘ 𝐺 )
5 eqid ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
6 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
7 1 2 5 6 3 subgrprop2 ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) )
8 3simpa ⊢ ( ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) → ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) )
9 7 8 syl ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) )
10 simprl ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) ) → 𝑉 ⊆ 𝐴 )
11 rnss ⊢ ( ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) → ran ( iEdg ‘ 𝑆 ) ⊆ ran ( iEdg ‘ 𝐺 ) )
12 11 ad2antll ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) ) → ran ( iEdg ‘ 𝑆 ) ⊆ ran ( iEdg ‘ 𝐺 ) )
13 subgrv ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) )
14 edgval ⊢ ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 )
15 14 a1i ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 ) )
16 3 15 eqtrid ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → 𝐸 = ran ( iEdg ‘ 𝑆 ) )
17 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
18 17 a1i ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
19 4 18 eqtrid ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → 𝐵 = ran ( iEdg ‘ 𝐺 ) )
20 16 19 sseq12d ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐸 ⊆ 𝐵 ↔ ran ( iEdg ‘ 𝑆 ) ⊆ ran ( iEdg ‘ 𝐺 ) ) )
21 13 20 syl ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝐸 ⊆ 𝐵 ↔ ran ( iEdg ‘ 𝑆 ) ⊆ ran ( iEdg ‘ 𝐺 ) ) )
22 21 adantr ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) ) → ( 𝐸 ⊆ 𝐵 ↔ ran ( iEdg ‘ 𝑆 ) ⊆ ran ( iEdg ‘ 𝐺 ) ) )
23 12 22 mpbird ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) ) → 𝐸 ⊆ 𝐵 )
24 10 23 jca ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ ( 𝑉 ⊆ 𝐴 ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) ) → ( 𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵 ) )
25 9 24 mpdan ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵 ) )