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 28447

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 2830	. . . . . 6 ⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ (Edg‘𝐺))
3		eqid 2738	. . . . . . 7 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
4	3	uhgredgiedgb 27399	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ (Edg‘𝐺) ↔ ∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))
5	2, 4	syl5bb 282	. . . . 5 ⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ 𝐸 ↔ ∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))
6	1	eleq2i 2830	. . . . . 6 ⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ (Edg‘𝐺))
7	3	uhgredgiedgb 27399	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ (Edg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)))
8	6, 7	syl5bb 282	. . . . 5 ⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ 𝐸 ↔ ∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)))
9	1	eleq2i 2830	. . . . . 6 ⊢ ({𝐶, 𝐴} ∈ 𝐸 ↔ {𝐶, 𝐴} ∈ (Edg‘𝐺))
10	3	uhgredgiedgb 27399	. . . . . 6 ⊢ (𝐺 ∈ UHGraph → ({𝐶, 𝐴} ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)))
11	9, 10	syl5bb 282	. . . . 5 ⊢ (𝐺 ∈ UHGraph → ({𝐶, 𝐴} ∈ 𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)))
12	5, 8, 11	3anbi123d 1434	. . . 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 2738	. . . . . . . . . . . . . 14 ⊢ ⟨“𝐴𝐵𝐶𝐴”⟩ = ⟨“𝐴𝐵𝐶𝐴”⟩
15		eqid 2738	. . . . . . . . . . . . . 14 ⊢ ⟨“𝑖𝑗𝑘”⟩ = ⟨“𝑖𝑗𝑘”⟩
16		3simpa 1146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))
17		pm3.22 459	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))
18	17	3adant2 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))
19	16, 18	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))
20	19	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))
21	20	ad2antlr 723	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))
22		3simpa 1146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶))
23		necom 2996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
24	23	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴)
25	24	anim1ci 615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴))
26	25	3adant2 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴))
27		necom 2996	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴)
28	27	biimpi 215	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ≠ 𝐶 → 𝐶 ≠ 𝐴)
29	28	3ad2ant2 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝐶 ≠ 𝐴)
30	22, 26, 29	3jca 1126	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴) ∧ 𝐶 ≠ 𝐴))
31	30	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴) ∧ 𝐶 ≠ 𝐴))
32	31	ad2antlr 723	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐴) ∧ 𝐶 ≠ 𝐴))
33		eqimss 3973	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖) → {𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖))
34	33	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) → {𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖))
35	34	3ad2ant3 1133	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → {𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖))
36		eqimss 3973	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗) → {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))
37	36	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) → {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))
38	37	3ad2ant1 1131	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))
39		eqimss 3973	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘) → {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘))
40	39	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) → {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘))
41	40	3ad2ant2 1132	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → {𝐶, 𝐴} ⊆ ((iEdg‘𝐺)‘𝑘))
42	35, 38, 41	3jca 1126	. . . . . . . . . . . . . . 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 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ 𝑉)
46		simp1 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑉)
47	45, 46	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))
48	47, 29	anim12i 612	. . . . . . . . . . . . . . . . 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 1129	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗))))
52	44, 1, 3	uhgr3cyclexlem 28446	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ 𝐶 ≠ 𝐴) ∧ ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)))) → 𝑖 ≠ 𝑗)
53	49, 51, 52	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑖 ≠ 𝑗)
54		3simpc 1148	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
55		simp3 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝐵 ≠ 𝐶)
56	54, 55	anim12i 612	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶))
57	56	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶))
58		3simpc 1148	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))) → ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖))))
59	44, 1, 3	uhgr3cyclexlem 28446	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) ∧ ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑘 ≠ 𝑖)
60	59	necomd 2998	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) ∧ ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑖 ≠ 𝑘)
61	57, 58, 60	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝑖 ≠ 𝑘)
62	44, 1, 3	uhgr3cyclexlem 28446	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)))) → 𝑗 ≠ 𝑘)
63	62	exp31 419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘)))
64	63	3adant3 1130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘)))
65	64	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ≠ 𝐵 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘))) → 𝑗 ≠ 𝑘)))
66	65	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . 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 1130	. . . . . . . . . . . . . . . 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 1126	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → (𝑖 ≠ 𝑗 ∧ 𝑖 ≠ 𝑘 ∧ 𝑗 ≠ 𝑘))
73		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → 𝐴 = 𝐴)
74	14, 15, 21, 32, 43, 44, 3, 72, 73	3cyclpd 28444	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) ∧ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) ∧ (𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)))) → (⟨“𝑖𝑗𝑘”⟩(Cycles‘𝐺)⟨“𝐴𝐵𝐶𝐴”⟩ ∧ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3 ∧ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴))
75		s3cli 14522	. . . . . . . . . . . . . . 15 ⊢ ⟨“𝑖𝑗𝑘”⟩ ∈ Word V
76	75	elexi 3441	. . . . . . . . . . . . . 14 ⊢ ⟨“𝑖𝑗𝑘”⟩ ∈ V
77		s4cli 14523	. . . . . . . . . . . . . . 15 ⊢ ⟨“𝐴𝐵𝐶𝐴”⟩ ∈ Word V
78	77	elexi 3441	. . . . . . . . . . . . . 14 ⊢ ⟨“𝐴𝐵𝐶𝐴”⟩ ∈ V
79		breq12 5075	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → (𝑓(Cycles‘𝐺)𝑝 ↔ ⟨“𝑖𝑗𝑘”⟩(Cycles‘𝐺)⟨“𝐴𝐵𝐶𝐴”⟩))
80		fveqeq2 6765	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ⟨“𝑖𝑗𝑘”⟩ → ((♯‘𝑓) = 3 ↔ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3))
81	80	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → ((♯‘𝑓) = 3 ↔ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3))
82		fveq1 6755	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩ → (𝑝‘0) = (⟨“𝐴𝐵𝐶𝐴”⟩‘0))
83	82	eqeq1d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩ → ((𝑝‘0) = 𝐴 ↔ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴))
84	83	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → ((𝑝‘0) = 𝐴 ↔ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴))
85	79, 81, 84	3anbi123d 1434	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = ⟨“𝑖𝑗𝑘”⟩ ∧ 𝑝 = ⟨“𝐴𝐵𝐶𝐴”⟩) → ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴) ↔ (⟨“𝑖𝑗𝑘”⟩(Cycles‘𝐺)⟨“𝐴𝐵𝐶𝐴”⟩ ∧ (♯‘⟨“𝑖𝑗𝑘”⟩) = 3 ∧ (⟨“𝐴𝐵𝐶𝐴”⟩‘0) = 𝐴)))
86	76, 78, 85	spc2ev 3536	. . . . . . . . . . . . 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 1117	. . . . . . . . . 10 ⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ {𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗)) → ((𝑘 ∈ dom (iEdg‘𝐺) ∧ {𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘)) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ {𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖)) → ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)))))
90	89	rexlimiva 3209	. . . . . . . . 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 3209	. . . . . . 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 3209	. . . . 5 ⊢ (∃𝑖 ∈ dom (iEdg‘𝐺){𝐴, 𝐵} = ((iEdg‘𝐺)‘𝑖) → (∃𝑗 ∈ dom (iEdg‘𝐺){𝐵, 𝐶} = ((iEdg‘𝐺)‘𝑗) → (∃𝑘 ∈ dom (iEdg‘𝐺){𝐶, 𝐴} = ((iEdg‘𝐺)‘𝑘) → ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)))))
95	94	3imp 1109	. . . 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 239	. 2 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)))
98	97	3impia 1115	1 ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∃wex 1783 ∈ wcel 2108 ≠ wne 2942 ∃wrex 3064 Vcvv 3422 ⊆ wss 3883 {cpr 4560 class class class wbr 5070 dom cdm 5580 ‘cfv 6418 0cc0 10802 3c3 11959 ♯chash 13972 Word cword 14145 ⟨“cs3 14483 ⟨“cs4 14484 Vtxcvtx 27269 iEdgciedg 27270 Edgcedg 27320 UHGraphcuhgr 27329 Cyclesccycls 28054

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-ifp 1060 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-fzo 13312 df-hash 13973 df-word 14146 df-concat 14202 df-s1 14229 df-s2 14489 df-s3 14490 df-s4 14491 df-edg 27321 df-uhgr 27331 df-wlks 27869 df-trls 27962 df-pths 27985 df-cycls 28056

This theorem is referenced by: umgr3cyclex 28448

W3C validator