Metamath Proof Explorer

Theorem uhgrwkspthlem2

Description: Lemma 2 for uhgrwkspth . (Contributed by AV, 25-Jan-2021)

Ref Expression
Assertion uhgrwkspthlem2 ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) = 1 ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → Fun ◡ 𝑃 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
3 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 1 ) )
4 1e0p1 ⊢ 1 = ( 0 + 1 )
5 4 oveq2i ⊢ ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
6 0z ⊢ 0 ∈ ℤ
7 fzpr ⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
8 6 7 ax-mp ⊢ ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
9 0p1e1 ⊢ ( 0 + 1 ) = 1
10 9 preq2i ⊢ { 0 , ( 0 + 1 ) } = { 0 , 1 }
11 5 8 10 3eqtri ⊢ ( 0 ... 1 ) = { 0 , 1 }
12 3 11 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } )
13 12 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ) )
14 13 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ) )
15 simpl ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
16 simpr ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 )
17 15 16 neeq12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ 𝐴 ≠ 𝐵 ) )
18 17 bicomd ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
19 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 1 ) )
20 19 neeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
21 18 20 sylan9bbr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
22 14 21 anbi12d ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) )
23 1z ⊢ 1 ∈ ℤ
24 fpr2g ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ↔ ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) ) )
25 6 23 24 mp2an ⊢ ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ↔ ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) )
26 funcnvs2 ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
27 26 3expa ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
28 27 adantl ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
29 simpl ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } )
30 s2prop ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } )
31 30 eqcomd ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
32 31 adantr ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
33 32 adantl ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
34 29 33 eqtrd ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → 𝑃 = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
35 34 cnveqd ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → ◡ 𝑃 = ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
36 35 funeqd ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → ( Fun ◡ 𝑃 ↔ Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ ) )
37 28 36 mpbird ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → Fun ◡ 𝑃 )
38 37 exp32 ⊢ ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) ) )
39 38 impcom ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) )
40 39 3impa ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) )
41 25 40 sylbi ⊢ ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) )
42 41 imp ⊢ ( ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → Fun ◡ 𝑃 )
43 22 42 syl6bi ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ 𝐵 ) → Fun ◡ 𝑃 ) )
44 43 expd ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝐴 ≠ 𝐵 → Fun ◡ 𝑃 ) ) )
45 44 com12 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝐴 ≠ 𝐵 → Fun ◡ 𝑃 ) ) )
46 45 expd ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝐹 ) = 1 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝐴 ≠ 𝐵 → Fun ◡ 𝑃 ) ) ) )
47 46 com34 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝐴 ≠ 𝐵 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → Fun ◡ 𝑃 ) ) ) )
48 47 impd ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → Fun ◡ 𝑃 ) ) )
49 2 48 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → Fun ◡ 𝑃 ) ) )
50 49 3imp ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) = 1 ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → Fun ◡ 𝑃 )