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 30144

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 2820	. . . . . 6 ⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ (Edg‘𝐺))
3		eqid 2729	. . . . . . 7 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
4	3	uhgredgiedgb 29089	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ (Edg‘𝐺) ↔ ∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))
5	2, 4	bitrid 283	. . . . 5 ⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ 𝐸 ↔ ∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))
6	1	eleq2i 2820	. . . . . 6 ⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ (Edg‘𝐺))
7	3	uhgredgiedgb 29089	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)))
8	6, 7	bitrid 283	. . . . 5 ⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ 𝐸 ↔ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)))
9	1	eleq2i 2820	. . . . . 6 ⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ (Edg‘𝐺))
10	3	uhgredgiedgb 29089	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐶, 𝐴} ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)))
11	9, 10	bitrid 283	. . . . 5 ⊢ (𝐺 ∈ UHGraph → ({𝐶, 𝐴} ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)))
12	5, 8, 11	3anbi123d 1438	. . . 4 ⊢ (𝐺 ∈ UHGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖) ∧ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗) ∧ ∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))))
13	12	adantr 480	. . 3 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ (∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖) ∧ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗) ∧ ∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))))
14		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ⟨“𝐴𝐵𝐶𝐴”⟩ = ⟨“𝐴𝐵𝐶𝐴”⟩
15		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ⟨“𝑖𝑗𝑘”⟩ = ⟨“𝑖𝑗𝑘”⟩
16		3simpa 1148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))
17		pm3.22 459	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))
18	17	3adant2 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))
19	16, 18	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))
20	19	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))
21	20	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))
22		3simpa 1148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶))
23		necom 2978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
24	23	biimpi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴)
25	24	anim1ci 616	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴))
26	25	3adant2 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴))
27		necom 2978	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
28	27	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ≠ 𝐶 → 𝐶 ≠ 𝐴)
29	28	3ad2ant2 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝐶 ≠ 𝐴)
30	22, 26, 29	3jca 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴) ∧ 𝐶 ≠ 𝐴))
31	30	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴) ∧ 𝐶 ≠ 𝐴))
32	31	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴) ∧ 𝐶 ≠ 𝐴))
33		eqimss 3996	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖) → {𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖))
34	33	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) → {𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖))
35	34	3ad2ant3 1135	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → {𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖))
36		eqimss 3996	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗) → {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))
37	36	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) → {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))
38	37	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))
39		eqimss 3996	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘) → {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘))
40	39	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) → {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘))
41	40	3ad2ant2 1134	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘))
42	35, 38, 41	3jca 1128	. . . . . . . . . . . . . . 15 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ({𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖) ∧ {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘)))
43	42	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → ({𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖) ∧ {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗) ∧ {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘)))
44		uhgr3cyclex.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (Vtx‘𝐺)
45		simp3 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ 𝑉)
46		simp1 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑉)
47	45, 46	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))
48	47, 29	anim12i 613	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ 𝐶 ≠ 𝐴))
49	48	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ 𝐶 ≠ 𝐴))
50		pm3.22 459	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗))))
51	50	3adant2 1131	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗))))
52	44, 1, 3	uhgr3cyclexlem 30143	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ 𝐶 ≠ 𝐴) ∧ ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)))) → 𝑖 ≠ 𝑗)
53	49, 51, 52	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑖 ≠ 𝑗)
54		3simpc 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
55		simp3 1138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝐵 ≠ 𝐶)
56	54, 55	anim12i 613	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶))
57	56	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶))
58		3simpc 1150	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))))
59	44, 1, 3	uhgr3cyclexlem 30143	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) ∧ ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑘 ≠ 𝑖)
60	59	necomd 2980	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) ∧ ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑖 ≠ 𝑘)
61	57, 58, 60	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑖 ≠ 𝑘)
62	44, 1, 3	uhgr3cyclexlem 30143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)))) → 𝑗 ≠ 𝑘)
63	62	exp31 419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘)))
64	63	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘)))
65	64	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ≠ 𝐵 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘)))
66	65	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘)))
67	66	impcom 407	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘))
68	67	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘))
69	68	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → 𝑗 ≠ 𝑘))
70	69	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → 𝑗 ≠ 𝑘))
71	70	impcom 407	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑗 ≠ 𝑘)
72	53, 61, 71	3jca 1128	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → (𝑖 ≠ 𝑗 ∧ 𝑖 ≠ 𝑘 ∧ 𝑗 ≠ 𝑘))
73		eqidd 2730	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝐴 = 𝐴)
74	14, 15, 21, 32, 43, 44, 3, 72, 73	3cyclpd 30141	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → (⟨“𝑖𝑗𝑘”⟩(Cycles‘𝐺)⟨“𝐴𝐵𝐶𝐴”⟩ ∧ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3 ∧ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴))
75		s3cli 14806	. . . . . . . . . . . . . . 15 ⊢ ⟨“𝑖𝑗𝑘”⟩ ∈ Word V
76	75	elexi 3461	. . . . . . . . . . . . . 14 ⊢ ⟨“𝑖𝑗𝑘”⟩ ∈ V
77		s4cli 14807	. . . . . . . . . . . . . . 15 ⊢ ⟨“𝐴𝐵𝐶𝐴”⟩ ∈ Word V
78	77	elexi 3461	. . . . . . . . . . . . . 14 ⊢ ⟨“𝐴𝐵𝐶𝐴”⟩ ∈ V
79		breq12 5100	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → (𝑓(Cycles‘𝐺)𝑝 ↔ ⟨“𝑖𝑗𝑘”⟩(Cycles‘𝐺)⟨“𝐴𝐵𝐶𝐴”⟩))
80		fveqeq2 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ⟨“𝑖𝑗𝑘”⟩ → ((♯‘𝑓) = 3 ↔ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3))
81	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → ((♯‘𝑓) = 3 ↔ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3))
82		fveq1 6825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩ → (𝑝‘0) = (⟨“𝐴𝐵𝐶𝐴”⟩‘0))
83	82	eqeq1d 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩ → ((𝑝‘0) = 𝐴 ↔ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴))
84	83	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → ((𝑝‘0) = 𝐴 ↔ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴))
85	79, 81, 84	3anbi123d 1438	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴) ↔ (⟨“𝑖𝑗𝑘”⟩(Cycles‘𝐺)⟨“𝐴𝐵𝐶𝐴”⟩ ∧ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3 ∧ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴)))
86	76, 78, 85	spc2ev 3564	. . . . . . . . . . . . 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 413	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)))
89	88	3exp 1119	. . . . . . . . . 10 ⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) → ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) → ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)))))
90	89	rexlimiva 3122	. . . . . . . . 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 3122	. . . . . . 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 3122	. . . . 5 ⊢ (∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖) → (∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗) → (∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘) → ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)))))
95	94	3imp 1110	. . . 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 240	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)))
98	97	3impia 1117	1 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 Vcvv 3438 ⊆ wss 3905 {cpr 4581 class class class wbr 5095 dom cdm 5623 ‘cfv 6486 0cc0 11028 3c3 12202 ♯chash 14255 Word cword 14438 ⟨“cs3 14767 ⟨“cs4 14768 Vtxcvtx 28959 iEdgciedg 28960 Edgcedg 29010 UHGraphcuhgr 29019 Cyclesccycls 29748

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ifp 1063 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8632 df-map 8762 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-n0 12403 df-z 12490 df-uz 12754 df-fz 13429 df-fzo 13576 df-hash 14256 df-word 14439 df-concat 14496 df-s1 14521 df-s2 14773 df-s3 14774 df-s4 14775 df-edg 29011 df-uhgr 29021 df-wlks 29563 df-trls 29654 df-pths 29677 df-cycls 29750

This theorem is referenced by: umgr3cyclex 30145

W3C validator