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

Metamath Proof Explorer

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 ffvelcdmd 
 |-  ( 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 ) )