Metamath Proof Explorer

Theorem wlkp1lem3

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 ∈ V
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
Assertion wlkp1lem3 ⊢ φ → iEdg ⁡ S ⁡ H ⁡ N = I ∪ B E ⁡ B

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 ∈ V
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 13 a1i ⊢ φ → H = F ∪ N B
15 14 fveq1d ⊢ φ → H ⁡ N = F ∪ N B ⁡ N
16 9 fvexi ⊢ N ∈ V
17 2 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
18 lencl ⊢ F ∈ Word dom ⁡ I → F ∈ ℕ 0
19 wrddm ⊢ F ∈ Word dom ⁡ I → dom ⁡ F = 0 ..^ F
20 fzonel ⊢ ¬ F ∈ 0 ..^ F
21 9 a1i ⊢ F ∈ ℕ 0 ∧ dom ⁡ F = 0 ..^ F → N = F
22 simpr ⊢ F ∈ ℕ 0 ∧ dom ⁡ F = 0 ..^ F → dom ⁡ F = 0 ..^ F
23 21 22 eleq12d ⊢ F ∈ ℕ 0 ∧ dom ⁡ F = 0 ..^ F → N ∈ dom ⁡ F ↔ F ∈ 0 ..^ F
24 20 23 mtbiri ⊢ F ∈ ℕ 0 ∧ dom ⁡ F = 0 ..^ F → ¬ N ∈ dom ⁡ F
25 18 19 24 syl2anc ⊢ F ∈ Word dom ⁡ I → ¬ N ∈ dom ⁡ F
26 8 17 25 3syl ⊢ φ → ¬ N ∈ dom ⁡ F
27 fsnunfv ⊢ N ∈ V ∧ B ∈ V ∧ ¬ N ∈ dom ⁡ F → F ∪ N B ⁡ N = B
28 16 5 26 27 mp3an2i ⊢ φ → F ∪ N B ⁡ N = B
29 15 28 eqtrd ⊢ φ → H ⁡ N = B
30 12 29 fveq12d ⊢ φ → iEdg ⁡ S ⁡ H ⁡ N = I ∪ B E ⁡ B