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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uhgr3cyclex.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	uhgr3cyclex	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		uhgr3cyclex.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uhgr3cyclex.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	2	eleq2i	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
4		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5	4	uhgredgiedgb	⊢ ( 𝐺 ∈ UHGraph → ( { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
6	3 5	syl5bb	⊢ ( 𝐺 ∈ UHGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
7	2	eleq2i	⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) )
8	4	uhgredgiedgb	⊢ ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
9	7 8	syl5bb	⊢ ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
10	2	eleq2i	⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) )
11	4	uhgredgiedgb	⊢ ( 𝐺 ∈ UHGraph → ( { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
12	10 11	syl5bb	⊢ ( 𝐺 ∈ UHGraph → ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
13	6 9 12	3anbi123d	⊢ ( 𝐺 ∈ UHGraph → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
14	13	adantr	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ↔ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
15		eqid	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ = ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩
16		eqid	⊢ ⟨“ 𝑖 𝑗 𝑘 ”⟩ = ⟨“ 𝑖 𝑗 𝑘 ”⟩
17		3simpa	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
18		pm3.22	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) )
19	18	3adant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) )
20	17 19	jca	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) )
21	20	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) )
22	21	ad2antlr	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) )
23		3simpa	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) )
24		necom	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
25	24	biimpi	⊢ ( 𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴 )
26	25	anim1ci	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ) )
27	26	3adant2	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ) )
28		necom	⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
29	28	biimpi	⊢ ( 𝐴 ≠ 𝐶 → 𝐶 ≠ 𝐴 )
30	29	3ad2ant2	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ≠ 𝐴 )
31	23 27 30	3jca	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐶 ≠ 𝐴 ) )
32	31	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐶 ≠ 𝐴 ) )
33	32	ad2antlr	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐶 ≠ 𝐴 ) )
34		eqimss	⊢ ( { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
35	34	adantl	⊢ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
36	35	3ad2ant3	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
37		eqimss	⊢ ( { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
38	37	adantl	⊢ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) → { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
39	38	3ad2ant1	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
40		eqimss	⊢ ( { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → { 𝐶 , 𝐴 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
41	40	adantl	⊢ ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → { 𝐶 , 𝐴 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
42	41	3ad2ant2	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → { 𝐶 , 𝐴 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
43	36 39 42	3jca	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐶 , 𝐴 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
44	43	adantl	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ { 𝐵 , 𝐶 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ { 𝐶 , 𝐴 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
45		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ 𝑉 )
46		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
47	45 46	jca	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) )
48	47 30	anim12i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐶 ≠ 𝐴 ) )
49	48	adantl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐶 ≠ 𝐴 ) )
50		pm3.22	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) )
51	50	3adant2	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) )
52	1 2 4	uhgr3cyclexlem	⊢ ( ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝐶 ≠ 𝐴 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ) → 𝑖 ≠ 𝑗 )
53	49 51 52	syl2an	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝑖 ≠ 𝑗 )
54		3simpc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
55		simp3	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ≠ 𝐶 )
56	54 55	anim12i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐵 ≠ 𝐶 ) )
57	56	adantl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐵 ≠ 𝐶 ) )
58		3simpc	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
59	1 2 4	uhgr3cyclexlem	⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐵 ≠ 𝐶 ) ∧ ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝑘 ≠ 𝑖 )
60	59	necomd	⊢ ( ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐵 ≠ 𝐶 ) ∧ ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝑖 ≠ 𝑘 )
61	57 58 60	syl2an	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝑖 ≠ 𝑘 )
62	1 2 4	uhgr3cyclexlem	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) ) → 𝑗 ≠ 𝑘 )
63	62	exp31	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐵 → ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) → 𝑗 ≠ 𝑘 ) ) )
64	63	3adant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐵 → ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) → 𝑗 ≠ 𝑘 ) ) )
65	64	com12	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) → 𝑗 ≠ 𝑘 ) ) )
66	65	3ad2ant1	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) → 𝑗 ≠ 𝑘 ) ) )
67	66	impcom	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) → 𝑗 ≠ 𝑘 ) )
68	67	adantl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) → 𝑗 ≠ 𝑘 ) )
69	68	com12	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → 𝑗 ≠ 𝑘 ) )
70	69	3adant3	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → 𝑗 ≠ 𝑘 ) )
71	70	impcom	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝑗 ≠ 𝑘 )
72	53 61 71	3jca	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝑖 ≠ 𝑗 ∧ 𝑖 ≠ 𝑘 ∧ 𝑗 ≠ 𝑘 ) )
73		eqidd	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝐴 = 𝐴 )
74	15 16 22 33 44 1 4 72 73	3cyclpd	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ⟨“ 𝑖 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) = 3 ∧ ( ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ‘ 0 ) = 𝐴 ) )
75		s3cli	⊢ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∈ Word V
76	75	elexi	⊢ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∈ V
77		s4cli	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ∈ Word V
78	77	elexi	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ∈ V
79		breq12	⊢ ( ( 𝑓 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ) )
80		fveqeq2	⊢ ( 𝑓 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ → ( ( ♯ ‘ 𝑓 ) = 3 ↔ ( ♯ ‘ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) = 3 ) )
81	80	adantr	⊢ ( ( 𝑓 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ) → ( ( ♯ ‘ 𝑓 ) = 3 ↔ ( ♯ ‘ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) = 3 ) )
82		fveq1	⊢ ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ‘ 0 ) )
83	82	eqeq1d	⊢ ( 𝑝 = ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ → ( ( 𝑝 ‘ 0 ) = 𝐴 ↔ ( ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ‘ 0 ) = 𝐴 ) )
84	83	adantl	⊢ ( ( 𝑓 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ) → ( ( 𝑝 ‘ 0 ) = 𝐴 ↔ ( ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ‘ 0 ) = 𝐴 ) )
85	79 81 84	3anbi123d	⊢ ( ( 𝑓 = ⟨“ 𝑖 𝑗 𝑘 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ) → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ↔ ( ⟨“ 𝑖 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) = 3 ∧ ( ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ‘ 0 ) = 𝐴 ) ) )
86	76 78 85	spc2ev	⊢ ( ( ⟨“ 𝑖 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ∧ ( ♯ ‘ ⟨“ 𝑖 𝑗 𝑘 ”⟩ ) = 3 ∧ ( ⟨“ 𝐴 𝐵 𝐶 𝐴 ”⟩ ‘ 0 ) = 𝐴 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) )
87	74 86	syl	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) ∧ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) )
88	87	expcom	⊢ ( ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) )
89	88	3exp	⊢ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) ) ) )
90	89	rexlimiva	⊢ ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) ) ) )
91	90	com12	⊢ ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) ) ) )
92	91	rexlimiva	⊢ ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) ) ) )
93	92	com13	⊢ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) ) ) )
94	93	rexlimiva	⊢ ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) ) ) )
95	94	3imp	⊢ ( ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) )
96	95	com12	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ( ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) )
97	14 96	sylbid	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) ) )
98	97	3impia	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ∧ { 𝐶 , 𝐴 } ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 3 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ) )