subgrpth

Description: If a path exists in a subgraph of a graph G , then that path also exists in G . (Contributed by BTernaryTau, 22-Oct-2023)

		Ref	Expression
	Assertion	subgrpth	$⊢ S SubGraph G \to (F Paths (S) P \to F Paths (G) P)$

Step	Hyp	Ref	Expression
1		subgrtrl	$⊢ S SubGraph G \to (F Trails (S) P \to F Trails (G) P)$
2		idd	$⊢ S SubGraph G \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})$
3		idd	$⊢ S SubGraph G \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
4	1 2 3	3anim123d	$⊢ S SubGraph G \to ((F Trails (S) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset))$
5		ispth	$⊢ F Paths (S) P \leftrightarrow (F Trails (S) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
6		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
7	4 5 6	3imtr4g	$⊢ S SubGraph G \to (F Paths (S) P \to F Paths (G) P)$

Metamath Proof Explorer