Metamath Proof Explorer

Theorem wlkp1lem5

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v ⊢ V = Vtx ⁡ G
wlkp1.i ⊢ I = iEdg ⁡ G
wlkp1.f ⊢ φ → Fun ⁡ I
wlkp1.a ⊢ φ → I ∈ Fin
wlkp1.b ⊢ φ → B ∈ W
wlkp1.c ⊢ φ → C ∈ V
wlkp1.d ⊢ φ → ¬ B ∈ dom ⁡ I
wlkp1.w ⊢ φ → F Walks ⁡ G P
wlkp1.n ⊢ N = F
wlkp1.e ⊢ φ → E ∈ Edg ⁡ G
wlkp1.x ⊢ φ → P ⁡ N C ⊆ E
wlkp1.u ⊢ φ → iEdg ⁡ S = I ∪ B E
wlkp1.h ⊢ H = F ∪ N B
wlkp1.q ⊢ Q = P ∪ N + 1 C
wlkp1.s ⊢ φ → Vtx ⁡ S = V
Assertion wlkp1lem5 ⊢ φ → ∀ k ∈ 0 … N Q ⁡ k = P ⁡ k

Proof

Step Hyp Ref Expression
1 wlkp1.v ⊢ V = Vtx ⁡ G
2 wlkp1.i ⊢ I = iEdg ⁡ G
3 wlkp1.f ⊢ φ → Fun ⁡ I
4 wlkp1.a ⊢ φ → I ∈ Fin
5 wlkp1.b ⊢ φ → B ∈ W
6 wlkp1.c ⊢ φ → C ∈ V
7 wlkp1.d ⊢ φ → ¬ B ∈ dom ⁡ I
8 wlkp1.w ⊢ φ → F Walks ⁡ G P
9 wlkp1.n ⊢ N = F
10 wlkp1.e ⊢ φ → E ∈ Edg ⁡ G
11 wlkp1.x ⊢ φ → P ⁡ N C ⊆ E
12 wlkp1.u ⊢ φ → iEdg ⁡ S = I ∪ B E
13 wlkp1.h ⊢ H = F ∪ N B
14 wlkp1.q ⊢ Q = P ∪ N + 1 C
15 wlkp1.s ⊢ φ → Vtx ⁡ S = V
16 14 fveq1i ⊢ Q ⁡ k = P ∪ N + 1 C ⁡ k
17 fzp1nel ⊢ ¬ N + 1 ∈ 0 … N
18 eleq1 ⊢ k = N + 1 → k ∈ 0 … N ↔ N + 1 ∈ 0 … N
19 18 notbid ⊢ k = N + 1 → ¬ k ∈ 0 … N ↔ ¬ N + 1 ∈ 0 … N
20 19 eqcoms ⊢ N + 1 = k → ¬ k ∈ 0 … N ↔ ¬ N + 1 ∈ 0 … N
21 17 20 mpbiri ⊢ N + 1 = k → ¬ k ∈ 0 … N
22 21 a1i ⊢ φ → N + 1 = k → ¬ k ∈ 0 … N
23 22 con2d ⊢ φ → k ∈ 0 … N → ¬ N + 1 = k
24 23 imp ⊢ φ ∧ k ∈ 0 … N → ¬ N + 1 = k
25 24 neqned ⊢ φ ∧ k ∈ 0 … N → N + 1 ≠ k
26 fvunsn ⊢ N + 1 ≠ k → P ∪ N + 1 C ⁡ k = P ⁡ k
27 25 26 syl ⊢ φ ∧ k ∈ 0 … N → P ∪ N + 1 C ⁡ k = P ⁡ k
28 16 27 syl5eq ⊢ φ ∧ k ∈ 0 … N → Q ⁡ k = P ⁡ k
29 28 ralrimiva ⊢ φ → ∀ k ∈ 0 … N Q ⁡ k = P ⁡ k