Metamath Proof Explorer


Theorem wlkp1lem4

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

Ref Expression
Hypotheses wlkp1.v 𝑉 = ( Vtx ‘ 𝐺 )
wlkp1.i 𝐼 = ( iEdg ‘ 𝐺 )
wlkp1.f ( 𝜑 → Fun 𝐼 )
wlkp1.a ( 𝜑𝐼 ∈ Fin )
wlkp1.b ( 𝜑𝐵𝑊 )
wlkp1.c ( 𝜑𝐶𝑉 )
wlkp1.d ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
wlkp1.w ( 𝜑𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
wlkp1.n 𝑁 = ( ♯ ‘ 𝐹 )
wlkp1.e ( 𝜑𝐸 ∈ ( Edg ‘ 𝐺 ) )
wlkp1.x ( 𝜑 → { ( 𝑃𝑁 ) , 𝐶 } ⊆ 𝐸 )
wlkp1.u ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
wlkp1.h 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
wlkp1.q 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
wlkp1.s ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
Assertion wlkp1lem4 ( 𝜑 → ( 𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )

Proof

Step Hyp Ref Expression
1 wlkp1.v 𝑉 = ( Vtx ‘ 𝐺 )
2 wlkp1.i 𝐼 = ( iEdg ‘ 𝐺 )
3 wlkp1.f ( 𝜑 → Fun 𝐼 )
4 wlkp1.a ( 𝜑𝐼 ∈ Fin )
5 wlkp1.b ( 𝜑𝐵𝑊 )
6 wlkp1.c ( 𝜑𝐶𝑉 )
7 wlkp1.d ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
8 wlkp1.w ( 𝜑𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9 wlkp1.n 𝑁 = ( ♯ ‘ 𝐹 )
10 wlkp1.e ( 𝜑𝐸 ∈ ( Edg ‘ 𝐺 ) )
11 wlkp1.x ( 𝜑 → { ( 𝑃𝑁 ) , 𝐶 } ⊆ 𝐸 )
12 wlkp1.u ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
13 wlkp1.h 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
14 wlkp1.q 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
15 wlkp1.s ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
16 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
17 16 wlkf ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
18 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
19 18 wlkp ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
20 17 19 jca ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
21 8 20 syl ( 𝜑 → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
22 6 15 eleqtrrd ( 𝜑𝐶 ∈ ( Vtx ‘ 𝑆 ) )
23 22 elfvexd ( 𝜑𝑆 ∈ V )
24 23 adantr ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → 𝑆 ∈ V )
25 simprl ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
26 snex { ⟨ 𝑁 , 𝐵 ⟩ } ∈ V
27 unexg ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ { ⟨ 𝑁 , 𝐵 ⟩ } ∈ V ) → ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ∈ V )
28 25 26 27 sylancl ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ∈ V )
29 13 28 eqeltrid ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → 𝐻 ∈ V )
30 ovex ( 0 ... ( ♯ ‘ 𝐹 ) ) ∈ V
31 fvex ( Vtx ‘ 𝐺 ) ∈ V
32 30 31 fpm ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑃 ∈ ( ( Vtx ‘ 𝐺 ) ↑pm ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
33 32 ad2antll ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → 𝑃 ∈ ( ( Vtx ‘ 𝐺 ) ↑pm ( 0 ... ( ♯ ‘ 𝐹 ) ) ) )
34 snex { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ∈ V
35 unexg ( ( 𝑃 ∈ ( ( Vtx ‘ 𝐺 ) ↑pm ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ∈ V ) → ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ∈ V )
36 33 34 35 sylancl ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ∈ V )
37 14 36 eqeltrid ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → 𝑄 ∈ V )
38 24 29 37 3jca ( ( 𝜑 ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ) → ( 𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )
39 21 38 mpdan ( 𝜑 → ( 𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )