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	syl5eq	⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → 𝐸 = ran ( iEdg ‘ 𝑆 ) )
17		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
18	17	a1i	⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
19	4 18	syl5eq	⊢ ( ( 𝑆 ∈ 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 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵 ) )

Metamath Proof Explorer

Theorem subgrprop3

Proof