This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0wlkonlem2

Description: Lemma 2 for 0wlkon and 0trlon . (Contributed by AV, 3-Jan-2021) (Revised by AV, 23-Mar-2021)

		Ref	Expression
	Hypothesis	0wlk.v	$⊢ V = Vtx (G)$
	Assertion	0wlkonlem2	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to P \in (V ↑_{𝑝𝑚} (0 \dots 0))$

Step	Hyp	Ref	Expression
1		0wlk.v	$⊢ V = Vtx (G)$
2		ovex	$⊢ (0 \dots 0) \in V$
3	1	fvexi	$⊢ V \in V$
4		simpl	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to P : (0 \dots 0) ⟶ V$
5		fpmg	$⊢ ((0 \dots 0) \in V \land V \in V \land P : (0 \dots 0) ⟶ V) \to P \in (V ↑_{𝑝𝑚} (0 \dots 0))$
6	2 3 4 5	mp3an12i	$⊢ (P : (0 \dots 0) ⟶ V \land P (0) = N) \to P \in (V ↑_{𝑝𝑚} (0 \dots 0))$