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 
|- ( ph -> G e. UPGraph )
cycl3grtri.c 
|- ( ph -> F ( Cycles ` G ) P )
cycl3grtri.n 
|- ( ph -> ( # ` F ) = 3 )
Assertion cycl3grtri 
|- ( ph -> ran P e. ( GrTriangles ` G ) )

Proof

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