Metamath Proof Explorer

Theorem subgrfun

Description: The edge function of a subgraph of a graph whose edge function is actually a function is a function. (Contributed by AV, 20-Nov-2020)

Ref Expression
Assertion subgrfun ⊢ Fun ⁡ iEdg ⁡ G ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ S = Vtx ⁡ S
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 eqid ⊢ Edg ⁡ S = Edg ⁡ S
6 1 2 3 4 5 subgrprop2 ⊢ S SubGraph G → Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
7 funss ⊢ iEdg ⁡ S ⊆ iEdg ⁡ G → Fun ⁡ iEdg ⁡ G → Fun ⁡ iEdg ⁡ S
8 7 3ad2ant2 ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → Fun ⁡ iEdg ⁡ G → Fun ⁡ iEdg ⁡ S
9 6 8 syl ⊢ S SubGraph G → Fun ⁡ iEdg ⁡ G → Fun ⁡ iEdg ⁡ S
10 9 impcom ⊢ Fun ⁡ iEdg ⁡ G ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S