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 fz01pr ⊢ ( 0 ... 1 ) = { 0 , 1 }
5 3 4 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } )
6 5 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ) )
7 6 adantr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ) )
8 simpl ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
9 simpr ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 )
10 8 9 neeq12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ 𝐴 ≠ 𝐵 ) )
11 10 bicomd ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
12 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 1 ) )
13 12 neeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
14 11 13 sylan9bbr ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
15 7 14 anbi12d ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) )
16 0z ⊢ 0 ∈ ℤ
17 1z ⊢ 1 ∈ ℤ
18 fpr2g ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ↔ ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) ) )
19 16 17 18 mp2an ⊢ ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ↔ ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) )
20 funcnvs2 ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
21 20 3expa ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
22 21 adantl ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
23 simpl ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } )
24 s2prop ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } )
25 24 eqcomd ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
26 25 adantr ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
27 26 adantl ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
28 23 27 eqtrd ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → 𝑃 = ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
29 28 cnveqd ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → ◡ 𝑃 = ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ )
30 29 funeqd ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → ( Fun ◡ 𝑃 ↔ Fun ◡ ⟨“ ( 𝑃 ‘ 0 ) ( 𝑃 ‘ 1 ) ”⟩ ) )
31 22 30 mpbird ⊢ ( ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ∧ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) → Fun ◡ 𝑃 )
32 31 exp32 ⊢ ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) ) )
33 32 impcom ⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) )
34 33 3impa ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑃 ‘ 1 ) ⟩ } ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) )
35 19 34 sylbi ⊢ ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) → Fun ◡ 𝑃 ) )
36 35 imp ⊢ ( ( 𝑃 : { 0 , 1 } ⟶ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → Fun ◡ 𝑃 )
37 15 36 biimtrdi ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ 𝐴 ≠ 𝐵 ) → Fun ◡ 𝑃 ) )
38 37 expd ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝐴 ≠ 𝐵 → Fun ◡ 𝑃 ) ) )
39 38 com12 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → ( 𝐴 ≠ 𝐵 → Fun ◡ 𝑃 ) ) )
40 39 expd ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝐹 ) = 1 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → ( 𝐴 ≠ 𝐵 → Fun ◡ 𝑃 ) ) ) )
41 40 com34 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝐴 ≠ 𝐵 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → Fun ◡ 𝑃 ) ) ) )
42 41 impd ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → Fun ◡ 𝑃 ) ) )
43 2 42 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) → Fun ◡ 𝑃 ) ) )
44 43 3imp ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) = 1 ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) → Fun ◡ 𝑃 )