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

Metamath Proof Explorer

Theorem cycl3grtri

Description: The vertices of a cycle of size 3 are a triangle in a graph. (Contributed by AV, 5-Oct-2025)

Ref Expression
Hypotheses cycl3grtri.g ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
cycl3grtri.c ⊢ ( 𝜑 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )
cycl3grtri.n ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = 3 )
Assertion cycl3grtri ( 𝜑 → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 cycl3grtri.g ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
2 cycl3grtri.c ⊢ ( 𝜑 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )
3 cycl3grtri.n ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = 3 )
4 cyclprop ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
5 tpeq1 ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → { 𝑥 , 𝑦 , 𝑧 } = { ( 𝑃 ‘ 0 ) , 𝑦 , 𝑧 } )
6 5 eqeq2d ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( ran 𝑃 = { 𝑥 , 𝑦 , 𝑧 } ↔ ran 𝑃 = { ( 𝑃 ‘ 0 ) , 𝑦 , 𝑧 } ) )
7 preq1 ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → { 𝑥 , 𝑦 } = { ( 𝑃 ‘ 0 ) , 𝑦 } )
8 7 eleq1d ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 0 ) , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ) )
9 preq1 ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → { 𝑥 , 𝑧 } = { ( 𝑃 ‘ 0 ) , 𝑧 } )
10 9 eleq1d ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) )
11 8 10 3anbi12d ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { ( 𝑃 ‘ 0 ) , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) )
12 6 11 3anbi13d ⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( ( ran 𝑃 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { ( 𝑃 ‘ 0 ) , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
13 tpeq2 ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → { ( 𝑃 ‘ 0 ) , 𝑦 , 𝑧 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , 𝑧 } )
14 13 eqeq2d ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , 𝑦 , 𝑧 } ↔ ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , 𝑧 } ) )
15 preq2 ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → { ( 𝑃 ‘ 0 ) , 𝑦 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
16 15 eleq1d ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → ( { ( 𝑃 ‘ 0 ) , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
17 preq1 ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → { 𝑦 , 𝑧 } = { ( 𝑃 ‘ 1 ) , 𝑧 } )
18 17 eleq1d ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → ( { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 1 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) )
19 16 18 3anbi13d ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → ( ( { ( 𝑃 ‘ 0 ) , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) )
20 14 19 3anbi13d ⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → ( ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { ( 𝑃 ‘ 0 ) , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , 𝑧 } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
21 tpeq3 ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , 𝑧 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
22 21 eqeq2d ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , 𝑧 } ↔ ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
23 preq2 ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 0 ) , 𝑧 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } )
24 23 eleq1d ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → ( { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
25 preq2 ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 1 ) , 𝑧 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
26 25 eleq1d ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → ( { ( 𝑃 ‘ 1 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
27 24 26 3anbi23d ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
28 22 27 3anbi13d ⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) → ( ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , 𝑧 } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
29 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
30 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
31 30 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
32 simpl ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
33 3nn0 ⊢ 3 ∈ ℕ0
34 0elfz ⊢ ( 3 ∈ ℕ0 → 0 ∈ ( 0 ... 3 ) )
35 33 34 ax-mp ⊢ 0 ∈ ( 0 ... 3 )
36 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 3 ) )
37 35 36 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
38 37 ad2antll ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
39 32 38 ffvelcdmd ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
40 39 ex ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) )
41 29 31 40 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ) )
43 42 imp ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
44 1nn0 ⊢ 1 ∈ ℕ0
45 1le3 ⊢ 1 ≤ 3
46 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 3 ) ↔ ( 1 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 1 ≤ 3 ) )
47 44 33 45 46 mpbir3an ⊢ 1 ∈ ( 0 ... 3 )
48 47 36 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 1 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
49 48 ad2antll ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
50 32 49 ffvelcdmd ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) )
51 50 ex ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) )
52 29 31 51 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) ) )
54 53 imp ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 ‘ 1 ) ∈ ( Vtx ‘ 𝐺 ) )
55 2nn0 ⊢ 2 ∈ ℕ0
56 2re ⊢ 2 ∈ ℝ
57 3re ⊢ 3 ∈ ℝ
58 2lt3 ⊢ 2 < 3
59 56 57 58 ltleii ⊢ 2 ≤ 3
60 elfz2nn0 ⊢ ( 2 ∈ ( 0 ... 3 ) ↔ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 2 ≤ 3 ) )
61 55 33 59 60 mpbir3an ⊢ 2 ∈ ( 0 ... 3 )
62 61 36 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 2 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
63 62 ad2antll ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → 2 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
64 32 63 ffvelcdmd ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) )
65 64 ex ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) )
66 29 31 65 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 𝑃 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) )
68 67 imp ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) )
69 fdm ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
70 elnn0uz ⊢ ( 3 ∈ ℕ0 ↔ 3 ∈ ( ℤ≥ ‘ 0 ) )
71 33 70 mpbi ⊢ 3 ∈ ( ℤ≥ ‘ 0 )
72 fzisfzounsn ⊢ ( 3 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 3 ) = ( ( 0 ..^ 3 ) ∪ { 3 } ) )
73 71 72 ax-mp ⊢ ( 0 ... 3 ) = ( ( 0 ..^ 3 ) ∪ { 3 } )
74 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
75 74 uneq1i ⊢ ( ( 0 ..^ 3 ) ∪ { 3 } ) = ( { 0 , 1 , 2 } ∪ { 3 } )
76 73 75 eqtri ⊢ ( 0 ... 3 ) = ( { 0 , 1 , 2 } ∪ { 3 } )
77 36 76 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( { 0 , 1 , 2 } ∪ { 3 } ) )
78 77 adantl ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( { 0 , 1 , 2 } ∪ { 3 } ) )
79 69 78 sylan9eq ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → dom 𝑃 = ( { 0 , 1 , 2 } ∪ { 3 } ) )
80 79 imaeq2d ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 “ dom 𝑃 ) = ( 𝑃 “ ( { 0 , 1 , 2 } ∪ { 3 } ) ) )
81 imadmrn ⊢ ( 𝑃 “ dom 𝑃 ) = ran 𝑃
82 imaundi ⊢ ( 𝑃 “ ( { 0 , 1 , 2 } ∪ { 3 } ) ) = ( ( 𝑃 “ { 0 , 1 , 2 } ) ∪ ( 𝑃 “ { 3 } ) )
83 80 81 82 3eqtr3g ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ran 𝑃 = ( ( 𝑃 “ { 0 , 1 , 2 } ) ∪ ( 𝑃 “ { 3 } ) ) )
84 ffn ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
85 84 adantr ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
86 85 38 49 63 fnimatpd ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 “ { 0 , 1 , 2 } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
87 nn0fz0 ⊢ ( 3 ∈ ℕ0 ↔ 3 ∈ ( 0 ... 3 ) )
88 33 87 mpbi ⊢ 3 ∈ ( 0 ... 3 )
89 88 36 eleqtrrid ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
90 89 adantl ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
91 fnsnfv ⊢ ( ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 3 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → { ( 𝑃 ‘ 3 ) } = ( 𝑃 “ { 3 } ) )
92 84 90 91 syl2an ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → { ( 𝑃 ‘ 3 ) } = ( 𝑃 “ { 3 } ) )
93 92 eqcomd ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 𝑃 “ { 3 } ) = { ( 𝑃 ‘ 3 ) } )
94 86 93 uneq12d ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ( 𝑃 “ { 0 , 1 , 2 } ) ∪ ( 𝑃 “ { 3 } ) ) = ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 3 ) } ) )
95 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 3 ) )
96 95 eqeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) )
97 sneq ⊢ ( ( 𝑃 ‘ 3 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 3 ) } = { ( 𝑃 ‘ 0 ) } )
98 97 eqcoms ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 3 ) } = { ( 𝑃 ‘ 0 ) } )
99 98 uneq2d ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 3 ) } ) = ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 0 ) } ) )
100 snsstp1 ⊢ { ( 𝑃 ‘ 0 ) } ⊆ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
101 100 a1i ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 0 ) } ⊆ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
102 ssequn2 ⊢ ( { ( 𝑃 ‘ 0 ) } ⊆ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 0 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
103 101 102 sylib ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 0 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
104 99 103 eqtrd ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 3 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
105 96 104 biimtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 3 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
106 105 impcom ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 3 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
107 106 adantl ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∪ { ( 𝑃 ‘ 3 ) } ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
108 83 94 107 3eqtrd ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
109 108 ex ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
110 29 31 109 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
111 110 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
112 111 imp ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
113 breq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 1 ≤ ( ♯ ‘ 𝐹 ) ↔ 1 ≤ 3 ) )
114 45 113 mpbiri ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → 1 ≤ ( ♯ ‘ 𝐹 ) )
115 114 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → 1 ≤ ( ♯ ‘ 𝐹 ) )
116 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )
117 cyclnumvtx ⊢ ( ( 1 ≤ ( ♯ ‘ 𝐹 ) ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ ran 𝑃 ) = ( ♯ ‘ 𝐹 ) )
118 115 116 117 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ♯ ‘ ran 𝑃 ) = ( ♯ ‘ 𝐹 ) )
119 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ♯ ‘ 𝐹 ) = 3 )
120 118 119 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ♯ ‘ ran 𝑃 ) = 3 )
121 cycl3grtrilem ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
122 1 121 sylanl1 ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
123 112 120 122 3jca ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ran 𝑃 = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
124 12 20 28 43 54 68 123 3rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐺 ) ( ran 𝑃 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) )
125 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
126 30 125 isgrtri ⊢ ( ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐺 ) ( ran 𝑃 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ran 𝑃 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) )
127 124 126 sylibr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) )
128 127 exp32 ⊢ ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ) ) )
129 128 com23 ⊢ ( ( 𝜑 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ) ) )
130 129 expcom ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝜑 → ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ) ) ) )
131 130 com24 ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝜑 → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ) ) ) )
132 131 imp ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝜑 → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ) ) )
133 4 132 syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝜑 → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ) ) )
134 133 com13 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) ) ) )
135 3 2 134 mp2d ⊢ ( 𝜑 → ran 𝑃 ∈ ( GrTriangles ‘ 𝐺 ) )