Theorem subgreldmiedg

Description: An element of the domain of the edge function of a subgraph is an element of the domain of the edge function of the supergraph. (Contributed by AV, 20-Nov-2020)

	Ref	Expression
Assertion	subgreldmiedg	⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
2		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3		eqid	⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
4		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5		eqid	⊢ ( Edg ‘ 𝑆 ) = ( Edg ‘ 𝑆 )
6	1 2 3 4 5	subgrprop2	⊢ ( 𝑆 SubGraph 𝐺 → ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) )
7		dmss	⊢ ( ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) → dom ( iEdg ‘ 𝑆 ) ⊆ dom ( iEdg ‘ 𝐺 ) )
8	7	3ad2ant2	⊢ ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) → dom ( iEdg ‘ 𝑆 ) ⊆ dom ( iEdg ‘ 𝐺 ) )
9	8	sseld	⊢ ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) → ( 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) → 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) ) )
10	6 9	syl	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) → 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) ) )
11	10	imp	⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) )