uhgr3cyclex - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > uhgr3cyclex		Structured version Visualization version GIF version

Theorem uhgr3cyclex 27705

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.)

**Hypotheses**
Ref	Expression
uhgr3cyclex.v	⊢ 𝑉 = (Vtx‘𝐺)
uhgr3cyclex.e	⊢ 𝐸 = (Edg‘𝐺)

**Assertion**
Ref	Expression
uhgr3cyclex	⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴))

Distinct variable groups: 𝐴,𝑓,𝑝 𝐵,𝑓,𝑝 𝐶,𝑓,𝑝 𝑓,𝐺,𝑝 Allowed substitution hints: 𝐸(𝑓,𝑝) 𝑉(𝑓,𝑝)

Proof of Theorem uhgr3cyclex Dummy variables 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∃wex 1742 ∈ wcel 2050 ≠ wne 2961 ∃wrex 3083 Vcvv 3409 ⊆ wss 3823 {cpr 4437 class class class wbr 4923 dom cdm 5401 ‘cfv 6182 0cc0 10329 3c3 11490 ♯chash 13499 Word cword 13666 ⟨“cs3 14060 ⟨“cs4 14061 Vtxcvtx 26478 iEdgciedg 26479 Edgcedg 26529 UHGraphcuhgr 26538 Cyclesccycls 27268

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10385 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-ifp 1044 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-1st 7495 df-2nd 7496 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-1o 7899 df-oadd 7903 df-er 8083 df-map 8202 df-en 8301 df-dom 8302 df-sdom 8303 df-fin 8304 df-card 9156 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-nn 11434 df-2 11497 df-3 11498 df-4 11499 df-n0 11702 df-z 11788 df-uz 12053 df-fz 12703 df-fzo 12844 df-hash 13500 df-word 13667 df-concat 13728 df-s1 13753 df-s2 14066 df-s3 14067 df-s4 14068 df-edg 26530 df-uhgr 26540 df-wlks 27078 df-trls 27174 df-pths 27199 df-cycls 27270

This theorem is referenced by: umgr3cyclex 27706

W3C validator