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 ∈ V ∧ N ∈ 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 ∈ ℕ 0
4 0elfz ⊢ 0 ∈ ℕ 0 → 0 ∈ 0 … 0
5 3 4 mp1i ⊢ P : 0 … 0 ⟶ V → 0 ∈ 0 … 0
6 2 5 ffvelrnd ⊢ P : 0 … 0 ⟶ V → P ⁡ 0 ∈ V
7 6 adantr ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → P ⁡ 0 ∈ V
8 eleq1 ⊢ N = P ⁡ 0 → N ∈ V ↔ P ⁡ 0 ∈ V
9 8 eqcoms ⊢ P ⁡ 0 = N → N ∈ V ↔ P ⁡ 0 ∈ V
10 9 adantl ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → N ∈ V ↔ P ⁡ 0 ∈ V
11 7 10 mpbird ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → N ∈ V
12 id ⊢ N ∈ V → N ∈ V
13 11 12 jccir ⊢ P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N → N ∈ V ∧ N ∈ V