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 ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ f ∃ 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 ↔ A B ∈ Edg ⁡ G
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 4 uhgredgiedgb ⊢ G ∈ UHGraph → A B ∈ Edg ⁡ G ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ i
6 3 5 syl5bb ⊢ G ∈ UHGraph → A B ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ i
7 2 eleq2i ⊢ B C ∈ E ↔ B C ∈ Edg ⁡ G
8 4 uhgredgiedgb ⊢ G ∈ UHGraph → B C ∈ Edg ⁡ G ↔ ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j
9 7 8 syl5bb ⊢ G ∈ UHGraph → B C ∈ E ↔ ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j
10 2 eleq2i ⊢ C A ∈ E ↔ C A ∈ Edg ⁡ G
11 4 uhgredgiedgb ⊢ G ∈ UHGraph → C A ∈ Edg ⁡ G ↔ ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k
12 10 11 syl5bb ⊢ G ∈ UHGraph → C A ∈ E ↔ ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k
13 6 9 12 3anbi123d ⊢ G ∈ UHGraph → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ i ∧ ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j ∧ ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k
14 13 adantr ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ i ∧ ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j ∧ ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k
15 eqid ⊢ ⟨“ ABCA ”⟩ = ⟨“ ABCA ”⟩
16 eqid ⊢ ⟨“ ijk ”⟩ = ⟨“ ijk ”⟩
17 3simpa ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V ∧ B ∈ V
18 pm3.22 ⊢ A ∈ V ∧ C ∈ V → C ∈ V ∧ A ∈ V
19 18 3adant2 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V ∧ A ∈ V
20 17 19 jca ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ∈ V
21 20 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ∈ V
22 21 ad2antlr ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ∈ 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 ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ B ≠ A ∧ C ≠ A
33 32 ad2antlr ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ 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 ⊆ iEdg ⁡ G ⁡ i
35 34 adantl ⊢ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → A B ⊆ iEdg ⁡ G ⁡ i
36 35 3ad2ant3 ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → A B ⊆ iEdg ⁡ G ⁡ i
37 eqimss ⊢ B C = iEdg ⁡ G ⁡ j → B C ⊆ iEdg ⁡ G ⁡ j
38 37 adantl ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j → B C ⊆ iEdg ⁡ G ⁡ j
39 38 3ad2ant1 ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → B C ⊆ iEdg ⁡ G ⁡ j
40 eqimss ⊢ C A = iEdg ⁡ G ⁡ k → C A ⊆ iEdg ⁡ G ⁡ k
41 40 adantl ⊢ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → C A ⊆ iEdg ⁡ G ⁡ k
42 41 3ad2ant2 ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → C A ⊆ iEdg ⁡ G ⁡ k
43 36 39 42 3jca ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → A B ⊆ iEdg ⁡ G ⁡ i ∧ B C ⊆ iEdg ⁡ G ⁡ j ∧ C A ⊆ iEdg ⁡ G ⁡ k
44 43 adantl ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → A B ⊆ iEdg ⁡ G ⁡ i ∧ B C ⊆ iEdg ⁡ G ⁡ j ∧ C A ⊆ iEdg ⁡ G ⁡ k
45 simp3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
46 simp1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V
47 45 46 jca ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V ∧ A ∈ V
48 47 30 anim12i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → C ∈ V ∧ A ∈ V ∧ C ≠ A
49 48 adantl ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → C ∈ V ∧ A ∈ V ∧ C ≠ A
50 pm3.22 ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j
51 50 3adant2 ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j
52 1 2 4 uhgr3cyclexlem ⊢ C ∈ V ∧ A ∈ V ∧ C ≠ A ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j → i ≠ j
53 49 51 52 syl2an ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → i ≠ j
54 3simpc ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → B ∈ V ∧ C ∈ V
55 simp3 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → B ≠ C
56 54 55 anim12i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → B ∈ V ∧ C ∈ V ∧ B ≠ C
57 56 adantl ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → B ∈ V ∧ C ∈ V ∧ B ≠ C
58 3simpc ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i
59 1 2 4 uhgr3cyclexlem ⊢ B ∈ V ∧ C ∈ V ∧ B ≠ C ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → k ≠ i
60 59 necomd ⊢ B ∈ V ∧ C ∈ V ∧ B ≠ C ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → i ≠ k
61 57 58 60 syl2an ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → i ≠ k
62 1 2 4 uhgr3cyclexlem ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → j ≠ k
63 62 exp31 ⊢ A ∈ V ∧ B ∈ V → A ≠ B → j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → j ≠ k
64 63 3adant3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ≠ B → j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → j ≠ k
65 64 com12 ⊢ A ≠ B → A ∈ V ∧ B ∈ V ∧ C ∈ V → j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → j ≠ k
66 65 3ad2ant1 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A ∈ V ∧ B ∈ V ∧ C ∈ V → j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → j ≠ k
67 66 impcom ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → j ≠ k
68 67 adantl ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → j ≠ k
69 68 com12 ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → j ≠ k
70 69 3adant3 ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → j ≠ k
71 70 impcom ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → j ≠ k
72 53 61 71 3jca ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → i ≠ j ∧ i ≠ k ∧ j ≠ k
73 eqidd ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → A = A
74 15 16 22 33 44 1 4 72 73 3cyclpd ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → ⟨“ ijk ”⟩ Cycles ⁡ G ⟨“ ABCA ”⟩ ∧ ⟨“ ijk ”⟩ = 3 ∧ ⟨“ ABCA ”⟩ ⁡ 0 = A
75 s3cli ⊢ ⟨“ ijk ”⟩ ∈ Word V
76 75 elexi ⊢ ⟨“ ijk ”⟩ ∈ V
77 s4cli ⊢ ⟨“ ABCA ”⟩ ∈ Word V
78 77 elexi ⊢ ⟨“ ABCA ”⟩ ∈ V
79 breq12 ⊢ f = ⟨“ ijk ”⟩ ∧ p = ⟨“ ABCA ”⟩ → f Cycles ⁡ G p ↔ ⟨“ ijk ”⟩ Cycles ⁡ G ⟨“ ABCA ”⟩
80 fveqeq2 ⊢ f = ⟨“ ijk ”⟩ → f = 3 ↔ ⟨“ ijk ”⟩ = 3
81 80 adantr ⊢ f = ⟨“ ijk ”⟩ ∧ p = ⟨“ ABCA ”⟩ → f = 3 ↔ ⟨“ ijk ”⟩ = 3
82 fveq1 ⊢ p = ⟨“ ABCA ”⟩ → p ⁡ 0 = ⟨“ ABCA ”⟩ ⁡ 0
83 82 eqeq1d ⊢ p = ⟨“ ABCA ”⟩ → p ⁡ 0 = A ↔ ⟨“ ABCA ”⟩ ⁡ 0 = A
84 83 adantl ⊢ f = ⟨“ ijk ”⟩ ∧ p = ⟨“ ABCA ”⟩ → p ⁡ 0 = A ↔ ⟨“ ABCA ”⟩ ⁡ 0 = A
85 79 81 84 3anbi123d ⊢ f = ⟨“ ijk ”⟩ ∧ p = ⟨“ ABCA ”⟩ → f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A ↔ ⟨“ ijk ”⟩ Cycles ⁡ G ⟨“ ABCA ”⟩ ∧ ⟨“ ijk ”⟩ = 3 ∧ ⟨“ ABCA ”⟩ ⁡ 0 = A
86 76 78 85 spc2ev ⊢ ⟨“ ijk ”⟩ Cycles ⁡ G ⟨“ ABCA ”⟩ ∧ ⟨“ ijk ”⟩ = 3 ∧ ⟨“ ABCA ”⟩ ⁡ 0 = A → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
87 74 86 syl ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
88 87 expcom ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j ∧ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k ∧ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
89 88 3exp ⊢ j ∈ dom ⁡ iEdg ⁡ G ∧ B C = iEdg ⁡ G ⁡ j → k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
90 89 rexlimiva ⊢ ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j → k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
91 90 com12 ⊢ k ∈ dom ⁡ iEdg ⁡ G ∧ C A = iEdg ⁡ G ⁡ k → ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j → i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
92 91 rexlimiva ⊢ ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k → ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j → i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
93 92 com13 ⊢ i ∈ dom ⁡ iEdg ⁡ G ∧ A B = iEdg ⁡ G ⁡ i → ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j → ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
94 93 rexlimiva ⊢ ∃ i ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ i → ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j → ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
95 94 3imp ⊢ ∃ i ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ i ∧ ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j ∧ ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k → G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
96 95 com12 ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ i ∈ dom ⁡ iEdg ⁡ G A B = iEdg ⁡ G ⁡ i ∧ ∃ j ∈ dom ⁡ iEdg ⁡ G B C = iEdg ⁡ G ⁡ j ∧ ∃ k ∈ dom ⁡ iEdg ⁡ G C A = iEdg ⁡ G ⁡ k → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
97 14 96 sylbid ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A
98 97 3impia ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ A B ∈ E ∧ B C ∈ E ∧ C A ∈ E → ∃ f ∃ p f Cycles ⁡ G p ∧ f = 3 ∧ p ⁡ 0 = A