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 ⊢ V = Vtx ⁡ S
subgrprop3.a ⊢ A = Vtx ⁡ G
subgrprop3.e ⊢ E = Edg ⁡ S
subgrprop3.b ⊢ B = Edg ⁡ G
Assertion subgrprop3 ⊢ S SubGraph G → V ⊆ A ∧ E ⊆ B

Proof

Step Hyp Ref Expression
1 subgrprop3.v ⊢ V = Vtx ⁡ S
2 subgrprop3.a ⊢ A = Vtx ⁡ G
3 subgrprop3.e ⊢ E = Edg ⁡ S
4 subgrprop3.b ⊢ B = Edg ⁡ G
5 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
6 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
7 1 2 5 6 3 subgrprop2 ⊢ S SubGraph G → V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ E ⊆ 𝒫 V
8 3simpa ⊢ V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ E ⊆ 𝒫 V → V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G
9 7 8 syl ⊢ S SubGraph G → V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G
10 simprl ⊢ S SubGraph G ∧ V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G → V ⊆ A
11 rnss ⊢ iEdg ⁡ S ⊆ iEdg ⁡ G → ran ⁡ iEdg ⁡ S ⊆ ran ⁡ iEdg ⁡ G
12 11 ad2antll ⊢ S SubGraph G ∧ V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G → ran ⁡ iEdg ⁡ S ⊆ ran ⁡ iEdg ⁡ G
13 subgrv ⊢ S SubGraph G → S ∈ V ∧ G ∈ V
14 edgval ⊢ Edg ⁡ S = ran ⁡ iEdg ⁡ S
15 14 a1i ⊢ S ∈ V ∧ G ∈ V → Edg ⁡ S = ran ⁡ iEdg ⁡ S
16 3 15 syl5eq ⊢ S ∈ V ∧ G ∈ V → E = ran ⁡ iEdg ⁡ S
17 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
18 17 a1i ⊢ S ∈ V ∧ G ∈ V → Edg ⁡ G = ran ⁡ iEdg ⁡ G
19 4 18 syl5eq ⊢ S ∈ V ∧ G ∈ V → B = ran ⁡ iEdg ⁡ G
20 16 19 sseq12d ⊢ S ∈ V ∧ G ∈ V → E ⊆ B ↔ ran ⁡ iEdg ⁡ S ⊆ ran ⁡ iEdg ⁡ G
21 13 20 syl ⊢ S SubGraph G → E ⊆ B ↔ ran ⁡ iEdg ⁡ S ⊆ ran ⁡ iEdg ⁡ G
22 21 adantr ⊢ S SubGraph G ∧ V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G → E ⊆ B ↔ ran ⁡ iEdg ⁡ S ⊆ ran ⁡ iEdg ⁡ G
23 12 22 mpbird ⊢ S SubGraph G ∧ V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G → E ⊆ B
24 10 23 jca ⊢ S SubGraph G ∧ V ⊆ A ∧ iEdg ⁡ S ⊆ iEdg ⁡ G → V ⊆ A ∧ E ⊆ B
25 9 24 mpdan ⊢ S SubGraph G → V ⊆ A ∧ E ⊆ B