Metamath Proof Explorer

Theorem uhgr3cyclex

Description: If there are three different vertices in a hypergraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017) (Revised by AV, 12-Feb-2021)

Ref Expression
Hypotheses uhgr3cyclex.v 
|- V = ( Vtx ` G )
uhgr3cyclex.e 
|- E = ( Edg ` G )
Assertion uhgr3cyclex 
|- ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )

Proof

Step Hyp Ref Expression
1 uhgr3cyclex.v 
 |-  V = ( Vtx ` G )
2 uhgr3cyclex.e 
 |-  E = ( Edg ` G )
3 2 eleq2i 
 |-  ( { A , B } e. E <-> { A , B } e. ( Edg ` G ) )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 4 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( { A , B } e. ( Edg ` G ) <-> E. i e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` i ) ) )
6 3 5 syl5bb 
 |-  ( G e. UHGraph -> ( { A , B } e. E <-> E. i e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` i ) ) )
7 2 eleq2i 
 |-  ( { B , C } e. E <-> { B , C } e. ( Edg ` G ) )
8 4 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( { B , C } e. ( Edg ` G ) <-> E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) ) )
9 7 8 syl5bb 
 |-  ( G e. UHGraph -> ( { B , C } e. E <-> E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) ) )
10 2 eleq2i 
 |-  ( { C , A } e. E <-> { C , A } e. ( Edg ` G ) )
11 4 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( { C , A } e. ( Edg ` G ) <-> E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) ) )
12 10 11 syl5bb 
 |-  ( G e. UHGraph -> ( { C , A } e. E <-> E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) ) )
13 6 9 12 3anbi123d 
 |-  ( G e. UHGraph -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( E. i e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` i ) /\ E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) /\ E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) ) ) )
14 13 adantr 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) <-> ( E. i e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` i ) /\ E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) /\ E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) ) ) )
15 eqid 
 |-  <" A B C A "> = <" A B C A ">
16 eqid 
 |-  <" i j k "> = <" i j k ">
17 3simpa 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( A e. V /\ B e. V ) )
18 pm3.22 
 |-  ( ( A e. V /\ C e. V ) -> ( C e. V /\ A e. V ) )
19 18 3adant2 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( C e. V /\ A e. V ) )
20 17 19 jca 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ A e. V ) ) )
21 20 adantr 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ A e. V ) ) )
22 21 ad2antlr 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ A e. V ) ) )
23 3simpa 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A =/= B /\ A =/= C ) )
24 necom 
 |-  ( A =/= B <-> B =/= A )
25 24 biimpi 
 |-  ( A =/= B -> B =/= A )
26 25 anim1ci 
 |-  ( ( A =/= B /\ B =/= C ) -> ( B =/= C /\ B =/= A ) )
27 26 3adant2 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( B =/= C /\ B =/= A ) )
28 necom 
 |-  ( A =/= C <-> C =/= A )
29 28 biimpi 
 |-  ( A =/= C -> C =/= A )
30 29 3ad2ant2 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> C =/= A )
31 23 27 30 3jca 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= A ) /\ C =/= A ) )
32 31 adantl 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= A ) /\ C =/= A ) )
33 32 ad2antlr 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= A ) /\ C =/= A ) )
34 eqimss 
 |-  ( { A , B } = ( ( iEdg ` G ) ` i ) -> { A , B } C_ ( ( iEdg ` G ) ` i ) )
35 34 adantl 
 |-  ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) -> { A , B } C_ ( ( iEdg ` G ) ` i ) )
36 35 3ad2ant3 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> { A , B } C_ ( ( iEdg ` G ) ` i ) )
37 eqimss 
 |-  ( { B , C } = ( ( iEdg ` G ) ` j ) -> { B , C } C_ ( ( iEdg ` G ) ` j ) )
38 37 adantl 
 |-  ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) -> { B , C } C_ ( ( iEdg ` G ) ` j ) )
39 38 3ad2ant1 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> { B , C } C_ ( ( iEdg ` G ) ` j ) )
40 eqimss 
 |-  ( { C , A } = ( ( iEdg ` G ) ` k ) -> { C , A } C_ ( ( iEdg ` G ) ` k ) )
41 40 adantl 
 |-  ( ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) -> { C , A } C_ ( ( iEdg ` G ) ` k ) )
42 41 3ad2ant2 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> { C , A } C_ ( ( iEdg ` G ) ` k ) )
43 36 39 42 3jca 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> ( { A , B } C_ ( ( iEdg ` G ) ` i ) /\ { B , C } C_ ( ( iEdg ` G ) ` j ) /\ { C , A } C_ ( ( iEdg ` G ) ` k ) ) )
44 43 adantl 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> ( { A , B } C_ ( ( iEdg ` G ) ` i ) /\ { B , C } C_ ( ( iEdg ` G ) ` j ) /\ { C , A } C_ ( ( iEdg ` G ) ` k ) ) )
45 simp3 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> C e. V )
46 simp1 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> A e. V )
47 45 46 jca 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( C e. V /\ A e. V ) )
48 47 30 anim12i 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( C e. V /\ A e. V ) /\ C =/= A ) )
49 48 adantl 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> ( ( C e. V /\ A e. V ) /\ C =/= A ) )
50 pm3.22 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) /\ ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) ) )
51 50 3adant2 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) /\ ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) ) )
52 1 2 4 uhgr3cyclexlem 
 |-  ( ( ( ( C e. V /\ A e. V ) /\ C =/= A ) /\ ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) /\ ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) ) ) -> i =/= j )
53 49 51 52 syl2an 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> i =/= j )
54 3simpc 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( B e. V /\ C e. V ) )
55 simp3 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> B =/= C )
56 54 55 anim12i 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( B e. V /\ C e. V ) /\ B =/= C ) )
57 56 adantl 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> ( ( B e. V /\ C e. V ) /\ B =/= C ) )
58 3simpc 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> ( ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) )
59 1 2 4 uhgr3cyclexlem 
 |-  ( ( ( ( B e. V /\ C e. V ) /\ B =/= C ) /\ ( ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> k =/= i )
60 59 necomd 
 |-  ( ( ( ( B e. V /\ C e. V ) /\ B =/= C ) /\ ( ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> i =/= k )
61 57 58 60 syl2an 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> i =/= k )
62 1 2 4 uhgr3cyclexlem 
 |-  ( ( ( ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) ) -> j =/= k )
63 62 exp31 
 |-  ( ( A e. V /\ B e. V ) -> ( A =/= B -> ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) -> j =/= k ) ) )
64 63 3adant3 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( A =/= B -> ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) -> j =/= k ) ) )
65 64 com12 
 |-  ( A =/= B -> ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) -> j =/= k ) ) )
66 65 3ad2ant1 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) -> j =/= k ) ) )
67 66 impcom 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) -> j =/= k ) )
68 67 adantl 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) -> j =/= k ) )
69 68 com12 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> j =/= k ) )
70 69 3adant3 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> j =/= k ) )
71 70 impcom 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> j =/= k )
72 53 61 71 3jca 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> ( i =/= j /\ i =/= k /\ j =/= k ) )
73 eqidd 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> A = A )
74 15 16 22 33 44 1 4 72 73 3cyclpd 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> ( <" i j k "> ( Cycles ` G ) <" A B C A "> /\ ( # ` <" i j k "> ) = 3 /\ ( <" A B C A "> ` 0 ) = A ) )
75 s3cli 
 |-  <" i j k "> e. Word _V
76 75 elexi 
 |-  <" i j k "> e. _V
77 s4cli 
 |-  <" A B C A "> e. Word _V
78 77 elexi 
 |-  <" A B C A "> e. _V
79 breq12 
 |-  ( ( f = <" i j k "> /\ p = <" A B C A "> ) -> ( f ( Cycles ` G ) p <-> <" i j k "> ( Cycles ` G ) <" A B C A "> ) )
80 fveqeq2 
 |-  ( f = <" i j k "> -> ( ( # ` f ) = 3 <-> ( # ` <" i j k "> ) = 3 ) )
81 80 adantr 
 |-  ( ( f = <" i j k "> /\ p = <" A B C A "> ) -> ( ( # ` f ) = 3 <-> ( # ` <" i j k "> ) = 3 ) )
82 fveq1 
 |-  ( p = <" A B C A "> -> ( p ` 0 ) = ( <" A B C A "> ` 0 ) )
83 82 eqeq1d 
 |-  ( p = <" A B C A "> -> ( ( p ` 0 ) = A <-> ( <" A B C A "> ` 0 ) = A ) )
84 83 adantl 
 |-  ( ( f = <" i j k "> /\ p = <" A B C A "> ) -> ( ( p ` 0 ) = A <-> ( <" A B C A "> ` 0 ) = A ) )
85 79 81 84 3anbi123d 
 |-  ( ( f = <" i j k "> /\ p = <" A B C A "> ) -> ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) <-> ( <" i j k "> ( Cycles ` G ) <" A B C A "> /\ ( # ` <" i j k "> ) = 3 /\ ( <" A B C A "> ` 0 ) = A ) ) )
86 76 78 85 spc2ev 
 |-  ( ( <" i j k "> ( Cycles ` G ) <" A B C A "> /\ ( # ` <" i j k "> ) = 3 /\ ( <" A B C A "> ` 0 ) = A ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )
87 74 86 syl 
 |-  ( ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) /\ ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )
88 87 expcom 
 |-  ( ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) /\ ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) /\ ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) )
89 88 3exp 
 |-  ( ( j e. dom ( iEdg ` G ) /\ { B , C } = ( ( iEdg ` G ) ` j ) ) -> ( ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) -> ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) ) ) )
90 89 rexlimiva 
 |-  ( E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) -> ( ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) -> ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) ) ) )
91 90 com12 
 |-  ( ( k e. dom ( iEdg ` G ) /\ { C , A } = ( ( iEdg ` G ) ` k ) ) -> ( E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) -> ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) ) ) )
92 91 rexlimiva 
 |-  ( E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) -> ( E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) -> ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) ) ) )
93 92 com13 
 |-  ( ( i e. dom ( iEdg ` G ) /\ { A , B } = ( ( iEdg ` G ) ` i ) ) -> ( E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) -> ( E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) ) ) )
94 93 rexlimiva 
 |-  ( E. i e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` i ) -> ( E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) -> ( E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) ) ) )
95 94 3imp 
 |-  ( ( E. i e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` i ) /\ E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) /\ E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) ) -> ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) )
96 95 com12 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> ( ( E. i e. dom ( iEdg ` G ) { A , B } = ( ( iEdg ` G ) ` i ) /\ E. j e. dom ( iEdg ` G ) { B , C } = ( ( iEdg ` G ) ` j ) /\ E. k e. dom ( iEdg ` G ) { C , A } = ( ( iEdg ` G ) ` k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) )
97 14 96 sylbid 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) ) -> ( ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) ) )
98 97 3impia 
 |-  ( ( G e. UHGraph /\ ( ( A e. V /\ B e. V /\ C e. V ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( { A , B } e. E /\ { B , C } e. E /\ { C , A } e. E ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )