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 ⊢ 𝑉 = ( 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 bitrid ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐴 , 𝐵 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
7 2 eleq2i ⊢ ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) )
8 4 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
9 7 8 bitrid ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐵 , 𝐶 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
10 2 eleq2i ⊢ ( { 𝐶 , 𝐴 } ∈ 𝐸 ↔ { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) )
11 4 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( { 𝐶 , 𝐴 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) { 𝐶 , 𝐴 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
12 10 11 bitrid ⊢ ( 𝐺 ∈ 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 ) = 𝐴 ) )