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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	0wlkonlem1	⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		id	⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
3		0nn0	⊢ 0 ∈ ℕ0
4		0elfz	⊢ ( 0 ∈ ℕ0 → 0 ∈ ( 0 ... 0 ) )
5	3 4	mp1i	⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 0 ∈ ( 0 ... 0 ) )
6	2 5	ffvelrnd	⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
7	6	adantr	⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
8		eleq1	⊢ ( 𝑁 = ( 𝑃 ‘ 0 ) → ( 𝑁 ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
9	8	eqcoms	⊢ ( ( 𝑃 ‘ 0 ) = 𝑁 → ( 𝑁 ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
10	9	adantl	⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
11	7 10	mpbird	⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑁 ∈ 𝑉 )
12		id	⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ 𝑉 )
13	11 12	jccir	⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )