This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elwwlks2

Description: A walk of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 21-Feb-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 14-Mar-2022)

Ref Expression
Hypothesis elwwlks2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion elwwlks2 ( 𝐺 ∈ UPGraph → ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elwwlks2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 wwlksnwwlksnon ⊢ ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 2 WWalksNOn 𝐺 ) 𝑐 ) )
3 2 a1i ⊢ ( 𝐺 ∈ UPGraph → ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 2 WWalksNOn 𝐺 ) 𝑐 ) ) )
4 1 elwwlks2on ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑊 ∈ ( 𝑎 ( 2 WWalksNOn 𝐺 ) 𝑐 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) )
5 4 3expb ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑊 ∈ ( 𝑎 ( 2 WWalksNOn 𝐺 ) 𝑐 ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) )
6 5 2rexbidva ⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 2 WWalksNOn 𝐺 ) 𝑐 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) )
7 rexcom ⊢ ( ∃ 𝑐 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ↔ ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
8 s3cli ⊢ ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word V
9 8 a1i ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∈ Word V )
10 simplr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
11 simpr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
12 10 11 eqtr4d ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → 𝑊 = 𝑝 )
13 12 breq2d ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ↔ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) )
14 13 biimpd ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) )
15 14 com12 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 → ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) )
16 15 adantr ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) )
17 16 impcom ⊢ ( ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 )
18 simprr ⊢ ( ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ♯ ‘ 𝑓 ) = 2 )
19 vex ⊢ 𝑎 ∈ V
20 s3fv0 ⊢ ( 𝑎 ∈ V → ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 0 ) = 𝑎 )
21 20 eqcomd ⊢ ( 𝑎 ∈ V → 𝑎 = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 0 ) )
22 19 21 mp1i ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → 𝑎 = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 0 ) )
23 fveq1 ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 0 ) )
24 22 23 eqtr4d ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → 𝑎 = ( 𝑝 ‘ 0 ) )
25 vex ⊢ 𝑏 ∈ V
26 s3fv1 ⊢ ( 𝑏 ∈ V → ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 1 ) = 𝑏 )
27 26 eqcomd ⊢ ( 𝑏 ∈ V → 𝑏 = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 1 ) )
28 25 27 mp1i ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → 𝑏 = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 1 ) )
29 fveq1 ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 1 ) )
30 28 29 eqtr4d ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → 𝑏 = ( 𝑝 ‘ 1 ) )
31 vex ⊢ 𝑐 ∈ V
32 s3fv2 ⊢ ( 𝑐 ∈ V → ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 2 ) = 𝑐 )
33 32 eqcomd ⊢ ( 𝑐 ∈ V → 𝑐 = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 2 ) )
34 31 33 mp1i ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → 𝑐 = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 2 ) )
35 fveq1 ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑝 ‘ 2 ) = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 2 ) )
36 34 35 eqtr4d ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → 𝑐 = ( 𝑝 ‘ 2 ) )
37 24 30 36 3jca ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) )
38 37 adantl ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) )
39 38 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) )
40 17 18 39 3jca ⊢ ( ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) )
41 40 ex ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ∧ 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) )
42 9 41 spcimedv ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) )
43 wlklenvp1 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
44 simpl ⊢ ( ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
45 oveq1 ⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( ( ♯ ‘ 𝑓 ) + 1 ) = ( 2 + 1 ) )
46 45 adantl ⊢ ( ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ♯ ‘ 𝑓 ) + 1 ) = ( 2 + 1 ) )
47 44 46 eqtrd ⊢ ( ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ♯ ‘ 𝑝 ) = ( 2 + 1 ) )
48 47 adantl ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ♯ ‘ 𝑝 ) = ( 2 + 1 ) )
49 2p1e3 ⊢ ( 2 + 1 ) = 3
50 48 49 eqtrdi ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ♯ ‘ 𝑝 ) = 3 )
51 50 exp32 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ♯ ‘ 𝑝 ) = ( ( ♯ ‘ 𝑓 ) + 1 ) → ( ( ♯ ‘ 𝑓 ) = 2 → ( ♯ ‘ 𝑝 ) = 3 ) ) )
52 43 51 mpd ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ♯ ‘ 𝑓 ) = 2 → ( ♯ ‘ 𝑝 ) = 3 ) )
53 52 adantr ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) → ( ( ♯ ‘ 𝑓 ) = 2 → ( ♯ ‘ 𝑝 ) = 3 ) )
54 53 imp ⊢ ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ♯ ‘ 𝑝 ) = 3 )
55 eqcom ⊢ ( 𝑎 = ( 𝑝 ‘ 0 ) ↔ ( 𝑝 ‘ 0 ) = 𝑎 )
56 55 biimpi ⊢ ( 𝑎 = ( 𝑝 ‘ 0 ) → ( 𝑝 ‘ 0 ) = 𝑎 )
57 eqcom ⊢ ( 𝑏 = ( 𝑝 ‘ 1 ) ↔ ( 𝑝 ‘ 1 ) = 𝑏 )
58 57 biimpi ⊢ ( 𝑏 = ( 𝑝 ‘ 1 ) → ( 𝑝 ‘ 1 ) = 𝑏 )
59 eqcom ⊢ ( 𝑐 = ( 𝑝 ‘ 2 ) ↔ ( 𝑝 ‘ 2 ) = 𝑐 )
60 59 biimpi ⊢ ( 𝑐 = ( 𝑝 ‘ 2 ) → ( 𝑝 ‘ 2 ) = 𝑐 )
61 56 58 60 3anim123i ⊢ ( ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) → ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ 1 ) = 𝑏 ∧ ( 𝑝 ‘ 2 ) = 𝑐 ) )
62 54 61 anim12i ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( ( ♯ ‘ 𝑝 ) = 3 ∧ ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ 1 ) = 𝑏 ∧ ( 𝑝 ‘ 2 ) = 𝑐 ) ) )
63 1 wlkpwrd ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → 𝑝 ∈ Word 𝑉 )
64 simpr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
65 64 anim1i ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
66 3anass ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( 𝑎 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
67 65 66 sylibr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) )
68 67 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) )
69 63 68 anim12i ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
70 69 ad2antrr ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑝 ∈ Word 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) )
71 eqwrds3 ⊢ ( ( 𝑝 ∈ Word 𝑉 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑝 ) = 3 ∧ ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ 1 ) = 𝑏 ∧ ( 𝑝 ‘ 2 ) = 𝑐 ) ) ) )
72 70 71 syl ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ↔ ( ( ♯ ‘ 𝑝 ) = 3 ∧ ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ 1 ) = 𝑏 ∧ ( 𝑝 ‘ 2 ) = 𝑐 ) ) ) )
73 62 72 mpbird ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → 𝑝 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
74 simprr ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) → 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
75 74 ad2antrr ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
76 73 75 eqtr4d ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → 𝑝 = 𝑊 )
77 76 breq2d ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ) )
78 77 biimpd ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ) )
79 simplr ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( ♯ ‘ 𝑓 ) = 2 )
80 78 79 jctird ⊢ ( ( ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) ) ∧ ( ♯ ‘ 𝑓 ) = 2 ) ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
81 80 exp41 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ( ♯ ‘ 𝑓 ) = 2 → ( ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) ) ) )
82 81 com25 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ♯ ‘ 𝑓 ) = 2 → ( ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) → ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) ) ) )
83 82 pm2.43i ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 → ( ( ♯ ‘ 𝑓 ) = 2 → ( ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) → ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) ) )
84 83 3imp ⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
85 84 com12 ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
86 85 exlimdv ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
87 42 86 impbid ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) )
88 87 exbidv ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) ∧ 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) )
89 88 pm5.32da ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ↔ ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) ) )
90 89 2rexbidva ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ↔ ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) ) )
91 7 90 bitrid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ↔ ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) ) )
92 91 rexbidva ⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) ) )
93 3 6 92 3bitrd ⊢ ( 𝐺 ∈ UPGraph → ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ∧ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ ( 𝑎 = ( 𝑝 ‘ 0 ) ∧ 𝑏 = ( 𝑝 ‘ 1 ) ∧ 𝑐 = ( 𝑝 ‘ 2 ) ) ) ) ) )