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 = ( Vtx ` G )
Assertion	0wlkonlem1	|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( N e. V /\ N e. V ) )

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	|- V = ( Vtx ` G )
2		id	|- ( P : ( 0 ... 0 ) --> V -> P : ( 0 ... 0 ) --> V )
3		0nn0	|- 0 e. NN0
4		0elfz	|- ( 0 e. NN0 -> 0 e. ( 0 ... 0 ) )
5	3 4	mp1i	|- ( P : ( 0 ... 0 ) --> V -> 0 e. ( 0 ... 0 ) )
6	2 5	ffvelrnd	|- ( P : ( 0 ... 0 ) --> V -> ( P ` 0 ) e. V )
7	6	adantr	|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( P ` 0 ) e. V )
8		eleq1	|- ( N = ( P ` 0 ) -> ( N e. V <-> ( P ` 0 ) e. V ) )
9	8	eqcoms	|- ( ( P ` 0 ) = N -> ( N e. V <-> ( P ` 0 ) e. V ) )
10	9	adantl	|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( N e. V <-> ( P ` 0 ) e. V ) )
11	7 10	mpbird	|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> N e. V )
12		id	|- ( N e. V -> N e. V )
13	11 12	jccir	|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( N e. V /\ N e. V ) )