Theorem subgrprop

Description: The properties of a subgraph. (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	subgrprop	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) )

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		subgrv	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) )
7	1 2 3 4 5	issubgr	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
8	7	biimpd	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
9	8	ancoms	⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
10	6 9	mpcom	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) )