Theorem subgrprop2

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 , connecting vertices of the subgraph only. (Contributed by AV, 19-Nov-2020)

	Ref	Expression
Hypotheses	issubgr.v	⊢ 𝑉 = ( Vtx ‘ 𝑆 )
	issubgr.a	⊢ 𝐴 = ( Vtx ‘ 𝐺 )
	issubgr.i	⊢ 𝐼 = ( iEdg ‘ 𝑆 )
	issubgr.b	⊢ 𝐵 = ( iEdg ‘ 𝐺 )
	issubgr.e	⊢ 𝐸 = ( Edg ‘ 𝑆 )
Assertion	subgrprop2	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		issubgr.v	⊢ 𝑉 = ( Vtx ‘ 𝑆 )
2		issubgr.a	⊢ 𝐴 = ( Vtx ‘ 𝐺 )
3		issubgr.i	⊢ 𝐼 = ( iEdg ‘ 𝑆 )
4		issubgr.b	⊢ 𝐵 = ( iEdg ‘ 𝐺 )
5		issubgr.e	⊢ 𝐸 = ( Edg ‘ 𝑆 )
6	1 2 3 4 5	subgrprop	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) )
7		resss	⊢ ( 𝐵 ↾ dom 𝐼 ) ⊆ 𝐵
8		sseq1	⊢ ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) → ( 𝐼 ⊆ 𝐵 ↔ ( 𝐵 ↾ dom 𝐼 ) ⊆ 𝐵 ) )
9	7 8	mpbiri	⊢ ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) → 𝐼 ⊆ 𝐵 )
10	9	3anim2i	⊢ ( ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) )
11	6 10	syl	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) )