Theorem loop1cycl 30678

Description: A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023.)

Assertion

Ref	Expression
loop1cycl	⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺)))

Distinct variable groups:   𝐺,𝑝   𝐴,𝑓,𝑝   𝑓,𝐺

Proof of Theorem loop1cycl

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cyclprop 30314	. . . . . . . . . . . . 13 ⊢ (𝑓(Cycles‘𝐺)𝑝 → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓))))
2		fveq2 6873	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑓) = 1 → (𝑝‘(♯‘𝑓)) = (𝑝‘1))
3	2	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑓) = 1 → ((𝑝‘0) = (𝑝‘(♯‘𝑓)) ↔ (𝑝‘0) = (𝑝‘1)))
4	3	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑓) = 1 → ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓))) ↔ (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))))
5	4	biimpd 232	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑓) = 1 → ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓))) → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1))))
6	1, 5	mpan9 516	. . . . . . . . . . . 12 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)))
7		pthiswlk 30244	. . . . . . . . . . . . 13 ⊢ (𝑓(Paths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝)
8	7	anim1i 627	. . . . . . . . . . . 12 ⊢ ((𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)))
9	6, 8	syl 18	. . . . . . . . . . 11 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)))
10	9	anim1i 627	. . . . . . . . . 10 ⊢ (((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) ∧ (♯‘𝑓) = 1) → ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1))
11	10	anabss3 688	. . . . . . . . 9 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1))
12		df-3an 1105	. . . . . . . . 9 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1) ↔ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1)) ∧ (♯‘𝑓) = 1))
13	11, 12	sylibr 237	. . . . . . . 8 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1))
14		3ancomb 1116	. . . . . . . 8 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘1) ∧ (♯‘𝑓) = 1) ↔ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1)))
15	13, 14	sylib 221	. . . . . . 7 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1)))
16		wlkl1loop 30152	. . . . . . . . . 10 ⊢ (((Fun (iEdg‘𝐺) ∧ 𝑓(Walks‘𝐺)𝑝) ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → {(𝑝‘0)} ∈ (Edg‘𝐺))
17	16	expl 463	. . . . . . . . 9 ⊢ (Fun (iEdg‘𝐺) → ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → {(𝑝‘0)} ∈ (Edg‘𝐺)))
18		eqid 2760	. . . . . . . . . 10 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
19	18	uhgrfun 29578	. . . . . . . . 9 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
20	17, 19	syl11 34	. . . . . . . 8 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1))) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺)))
21	20	3impb 1132	. . . . . . 7 ⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = (𝑝‘1)) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺)))
22	15, 21	syl 18	. . . . . 6 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺)))
23	22	3adant3 1150	. . . . 5 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {(𝑝‘0)} ∈ (Edg‘𝐺)))
24		sneq 4593	. . . . . . 7 ⊢ ((𝑝‘0) = 𝐴 → {(𝑝‘0)} = {𝐴})
25	24	eleq1d 2845	. . . . . 6 ⊢ ((𝑝‘0) = 𝐴 → ({(𝑝‘0)} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ (Edg‘𝐺)))
26	25	3ad2ant3 1153	. . . . 5 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → ({(𝑝‘0)} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ (Edg‘𝐺)))
27	23, 26	sylibd 242	. . . 4 ⊢ ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {𝐴} ∈ (Edg‘𝐺)))
28	27	exlimivv 1965	. . 3 ⊢ (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → (𝐺 ∈ UHGraph → {𝐴} ∈ (Edg‘𝐺)))
29	28	com12 33	. 2 ⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → {𝐴} ∈ (Edg‘𝐺)))
30		edgval 29561	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
31	30	eleq2i 2852	. . . . . . . . . . . . 13 ⊢ ({𝐴} ∈ (Edg‘𝐺) ↔ {𝐴} ∈ ran (iEdg‘𝐺))
32		elrnrexdm 7077	. . . . . . . . . . . . . 14 ⊢ (Fun (iEdg‘𝐺) → ({𝐴} ∈ ran (iEdg‘𝐺) → ∃𝑗 ∈ dom (iEdg‘𝐺){𝐴} = ((iEdg‘𝐺)‘𝑗)))
33		eqcom 2767	. . . . . . . . . . . . . . 15 ⊢ ({𝐴} = ((iEdg‘𝐺)‘𝑗) ↔ ((iEdg‘𝐺)‘𝑗) = {𝐴})
34	33	rexbii 3109	. . . . . . . . . . . . . 14 ⊢ (∃𝑗 ∈ dom (iEdg‘𝐺){𝐴} = ((iEdg‘𝐺)‘𝑗) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴})
35	32, 34	imbitrdi 254	. . . . . . . . . . . . 13 ⊢ (Fun (iEdg‘𝐺) → ({𝐴} ∈ ran (iEdg‘𝐺) → ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴}))
36	31, 35	biimtrid 245	. . . . . . . . . . . 12 ⊢ (Fun (iEdg‘𝐺) → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴}))
37	19, 36	syl 18	. . . . . . . . . . 11 ⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴}))
38		df-rex 3087	. . . . . . . . . . 11 ⊢ (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐴} ↔ ∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}))
39	37, 38	imbitrdi 254	. . . . . . . . . 10 ⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴})))
40	18	lp1cycl 30677	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → ⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩)
41	40	3expib 1140	. . . . . . . . . . 11 ⊢ (𝐺 ∈ UHGraph → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → ⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩))
42	41	eximdv 1950	. . . . . . . . . 10 ⊢ (𝐺 ∈ UHGraph → (∃𝑗(𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = {𝐴}) → ∃𝑗⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩))
43	39, 42	syld 48	. . . . . . . . 9 ⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩))
44		s1len 14721	. . . . . . . . . . 11 ⊢ (♯‘⟨“𝑗”⟩) = 1
45	44	ax-gen 1828	. . . . . . . . . 10 ⊢ ∀𝑗(♯‘⟨“𝑗”⟩) = 1
46		19.29r 1907	. . . . . . . . . 10 ⊢ ((∃𝑗⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ ∀𝑗(♯‘⟨“𝑗”⟩) = 1) → ∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1))
47	45, 46	mpan2 704	. . . . . . . . 9 ⊢ (∃𝑗⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ → ∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1))
48	43, 47	syl6 36	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1)))
49	48	imp 412	. . . . . . 7 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1))
50		uhgredgn0 29640	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → {𝐴} ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}))
51		eldifsni 4752	. . . . . . . . . . 11 ⊢ ({𝐴} ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) → {𝐴} ≠ ∅)
52	50, 51	syl 18	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → {𝐴} ≠ ∅)
53		snnzb 4678	. . . . . . . . . 10 ⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅)
54	52, 53	sylibr 237	. . . . . . . . 9 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → 𝐴 ∈ V)
55		s2fv0 15006	. . . . . . . . 9 ⊢ (𝐴 ∈ V → (⟨“𝐴𝐴”⟩‘0) = 𝐴)
56	54, 55	syl 18	. . . . . . . 8 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → (⟨“𝐴𝐴”⟩‘0) = 𝐴)
57	56	alrimiv 1960	. . . . . . 7 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∀𝑗(⟨“𝐴𝐴”⟩‘0) = 𝐴)
58		19.29r 1907	. . . . . . 7 ⊢ ((∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1) ∧ ∀𝑗(⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑗((⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1) ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
59	49, 57, 58	syl2anc 596	. . . . . 6 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗((⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1) ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
60		df-3an 1105	. . . . . . 7 ⊢ ((⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) ↔ ((⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1) ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
61	60	exbii 1881	. . . . . 6 ⊢ (∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) ↔ ∃𝑗((⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1) ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
62	59, 61	sylibr 237	. . . . 5 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
63		s1cli 14720	. . . . . . . 8 ⊢ ⟨“𝑗”⟩ ∈ Word V
64		breq1 5105	. . . . . . . . . 10 ⊢ (𝑓 = ⟨“𝑗”⟩ → (𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ↔ ⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩))
65		fveqeq2 6882	. . . . . . . . . 10 ⊢ (𝑓 = ⟨“𝑗”⟩ → ((♯‘𝑓) = 1 ↔ (♯‘⟨“𝑗”⟩) = 1))
66	64, 65	3anbi12d 1465	. . . . . . . . 9 ⊢ (𝑓 = ⟨“𝑗”⟩ → ((𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) ↔ (⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴)))
67	66	rspcev 3576	. . . . . . . 8 ⊢ ((⟨“𝑗”⟩ ∈ Word V ∧ (⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴)) → ∃𝑓 ∈ Word V(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
68	63, 67	mpan 703	. . . . . . 7 ⊢ ((⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑓 ∈ Word V(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
69		rexex 3092	. . . . . . 7 ⊢ (∃𝑓 ∈ Word V(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
70	68, 69	syl 18	. . . . . 6 ⊢ ((⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
71	70	exlimiv 1963	. . . . 5 ⊢ (∃𝑗(⟨“𝑗”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘⟨“𝑗”⟩) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑓(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
72	62, 71	syl 18	. . . 4 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑓(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
73		s2cli 14999	. . . . . . 7 ⊢ ⟨“𝐴𝐴”⟩ ∈ Word V
74		breq2 5106	. . . . . . . . 9 ⊢ (𝑝 = ⟨“𝐴𝐴”⟩ → (𝑓(Cycles‘𝐺)𝑝 ↔ 𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩))
75		fveq1 6872	. . . . . . . . . 10 ⊢ (𝑝 = ⟨“𝐴𝐴”⟩ → (𝑝‘0) = (⟨“𝐴𝐴”⟩‘0))
76	75	eqeq1d 2762	. . . . . . . . 9 ⊢ (𝑝 = ⟨“𝐴𝐴”⟩ → ((𝑝‘0) = 𝐴 ↔ (⟨“𝐴𝐴”⟩‘0) = 𝐴))
77	74, 76	3anbi13d 1466	. . . . . . . 8 ⊢ (𝑝 = ⟨“𝐴𝐴”⟩ → ((𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ (𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴)))
78	77	rspcev 3576	. . . . . . 7 ⊢ ((⟨“𝐴𝐴”⟩ ∈ Word V ∧ (𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴)) → ∃𝑝 ∈ Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))
79	73, 78	mpan 703	. . . . . 6 ⊢ ((𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑝 ∈ Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))
80		rexex 3092	. . . . . 6 ⊢ (∃𝑝 ∈ Word V(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) → ∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))
81	79, 80	syl 18	. . . . 5 ⊢ ((𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))
82	81	eximi 1868	. . . 4 ⊢ (∃𝑓(𝑓(Cycles‘𝐺)⟨“𝐴𝐴”⟩ ∧ (♯‘𝑓) = 1 ∧ (⟨“𝐴𝐴”⟩‘0) = 𝐴) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))
83	72, 82	syl 18	. . 3 ⊢ ((𝐺 ∈ UHGraph ∧ {𝐴} ∈ (Edg‘𝐺)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴))
84	83	ex 418	. 2 ⊢ (𝐺 ∈ UHGraph → ({𝐴} ∈ (Edg‘𝐺) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴)))
85	29, 84	impbid 215	1 ⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2955  ∃wrex 3086  Vcvv 3450   ∖ cdif 3895  ∅c0 4278  𝒫 cpw 4556  {csn 4583   class class class wbr 5102  dom cdm 5647  ran crn 5648  Fun wfun 6521  ‘cfv 6527  0cc0 11172  1c1 11173  ♯chash 14442  Word cword 14626  ⟨“cs1 14710  ⟨“cs2 14960  Vtxcvtx 29508  iEdgciedg 29509  Edgcedg 29559  UHGraphcuhgr 29568  Walkscwlks 30111  Pathscpths 30229  Cyclesccycls 30306

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11228  ax-resscn 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-addrcl 11233  ax-mulcl 11234  ax-mulrcl 11235  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-i2m1 11240  ax-1ne0 11241  ax-1rid 11242  ax-rnegex 11243  ax-rrecex 11244  ax-cnre 11245  ax-pre-lttri 11246  ax-pre-lttrn 11247  ax-pre-ltadd 11248  ax-pre-mulgt0 11249

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8454  df-er 8695  df-map 8827  df-pm 8828  df-en 8952  df-dom 8953  df-sdom 8954  df-fin 8955  df-card 9992  df-pnf 11317  df-mnf 11318  df-xr 11319  df-ltxr 11320  df-le 11321  df-sub 11515  df-neg 11516  df-nn 12306  df-2 12375  df-n0 12577  df-z 12664  df-uz 12936  df-fz 13610  df-fzo 13758  df-hash 14443  df-word 14627  df-concat 14684  df-s1 14711  df-s2 14967  df-edg 29560  df-uhgr 29570  df-wlks 30114  df-wlkson 30115  df-trls 30209  df-trlson 30210  df-pths 30233  df-pthson 30235  df-cycls 30308

This theorem is used by:  acycgrislfgr  35838