Theorem 0wlkonlem1

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

	Ref	Expression
Hypothesis	0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	0wlkonlem1	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to \left(N\in V\wedge N\in V\right)$$

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		id	$$⊢P:\left(0\dots 0\right)⟶V\to P:\left(0\dots 0\right)⟶V$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		0elfz	$$⊢0\in {\mathbb{N}}_0\to 0\in \left(0\dots 0\right)$$
5	3 4	mp1i	$$⊢P:\left(0\dots 0\right)⟶V\to 0\in \left(0\dots 0\right)$$
6	2 5	ffvelcdmd	$$⊢P:\left(0\dots 0\right)⟶V\to P\left(0\right)\in V$$
7	6	adantr	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to P\left(0\right)\in V$$
8		eleq1	$$⊢N=P\left(0\right)\to \left(N\in V\leftrightarrow P\left(0\right)\in V\right)$$
9	8	eqcoms	$$⊢P\left(0\right)=N\to \left(N\in V\leftrightarrow P\left(0\right)\in V\right)$$
10	9	adantl	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to \left(N\in V\leftrightarrow P\left(0\right)\in V\right)$$
11	7 10	mpbird	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to N\in V$$
12		id	$$⊢N\in V\to N\in V$$
13	11 12	jccir	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to \left(N\in V\wedge N\in V\right)$$