loop1cycl

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

		Ref	Expression
	Assertion	loop1cycl	$⊢ G \in UHGraph \to (\exists f \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \leftrightarrow \{A\} \in Edg (G))$

Proof

Step	Hyp	Ref	Expression
1		cyclprop	$⊢ f Cycles (G) p \to (f Paths (G) p \land p (0) = p (\|f\|))$
2		fveq2	$⊢ \|f\| = 1 \to p (\|f\|) = p (1)$
3	2	eqeq2d	$⊢ \|f\| = 1 \to (p (0) = p (\|f\|) \leftrightarrow p (0) = p (1))$
4	3	anbi2d	$⊢ \|f\| = 1 \to ((f Paths (G) p \land p (0) = p (\|f\|)) \leftrightarrow (f Paths (G) p \land p (0) = p (1)))$
5	4	biimpd	$⊢ \|f\| = 1 \to ((f Paths (G) p \land p (0) = p (\|f\|)) \to (f Paths (G) p \land p (0) = p (1)))$
6	1 5	mpan9	$⊢ (f Cycles (G) p \land \|f\| = 1) \to (f Paths (G) p \land p (0) = p (1))$
7		pthiswlk	$⊢ f Paths (G) p \to f Walks (G) p$
8	7	anim1i	$⊢ (f Paths (G) p \land p (0) = p (1)) \to (f Walks (G) p \land p (0) = p (1))$
9	6 8	syl	$⊢ (f Cycles (G) p \land \|f\| = 1) \to (f Walks (G) p \land p (0) = p (1))$
10	9	anim1i	$⊢ ((f Cycles (G) p \land \|f\| = 1) \land \|f\| = 1) \to ((f Walks (G) p \land p (0) = p (1)) \land \|f\| = 1)$
11	10	anabss3	$⊢ (f Cycles (G) p \land \|f\| = 1) \to ((f Walks (G) p \land p (0) = p (1)) \land \|f\| = 1)$
12		df-3an	$⊢ (f Walks (G) p \land p (0) = p (1) \land \|f\| = 1) \leftrightarrow ((f Walks (G) p \land p (0) = p (1)) \land \|f\| = 1)$
13	11 12	sylibr	$⊢ (f Cycles (G) p \land \|f\| = 1) \to (f Walks (G) p \land p (0) = p (1) \land \|f\| = 1)$
14		3ancomb	$⊢ (f Walks (G) p \land p (0) = p (1) \land \|f\| = 1) \leftrightarrow (f Walks (G) p \land \|f\| = 1 \land p (0) = p (1))$
15	13 14	sylib	$⊢ (f Cycles (G) p \land \|f\| = 1) \to (f Walks (G) p \land \|f\| = 1 \land p (0) = p (1))$
16		wlkl1loop	$⊢ ((Fun iEdg (G) \land f Walks (G) p) \land (\|f\| = 1 \land p (0) = p (1))) \to \{p (0)\} \in Edg (G)$
17	16	expl	$⊢ Fun iEdg (G) \to ((f Walks (G) p \land (\|f\| = 1 \land p (0) = p (1))) \to \{p (0)\} \in Edg (G))$
18		eqid	$⊢ iEdg (G) = iEdg (G)$
19	18	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
20	17 19	syl11	$⊢ (f Walks (G) p \land (\|f\| = 1 \land p (0) = p (1))) \to (G \in UHGraph \to \{p (0)\} \in Edg (G))$
21	20	3impb	$⊢ (f Walks (G) p \land \|f\| = 1 \land p (0) = p (1)) \to (G \in UHGraph \to \{p (0)\} \in Edg (G))$
22	15 21	syl	$⊢ (f Cycles (G) p \land \|f\| = 1) \to (G \in UHGraph \to \{p (0)\} \in Edg (G))$
23	22	3adant3	$⊢ (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \to (G \in UHGraph \to \{p (0)\} \in Edg (G))$
24		sneq	$⊢ p (0) = A \to \{p (0)\} = \{A\}$
25	24	eleq1d	$⊢ p (0) = A \to (\{p (0)\} \in Edg (G) \leftrightarrow \{A\} \in Edg (G))$
26	25	3ad2ant3	$⊢ (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \to (\{p (0)\} \in Edg (G) \leftrightarrow \{A\} \in Edg (G))$
27	23 26	sylibd	$⊢ (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \to (G \in UHGraph \to \{A\} \in Edg (G))$
28	27	exlimivv	$⊢ \exists f \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \to (G \in UHGraph \to \{A\} \in Edg (G))$
29	28	com12	$⊢ G \in UHGraph \to (\exists f \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \to \{A\} \in Edg (G))$
30		edgval	$⊢ Edg (G) = ran iEdg (G)$
31	30	eleq2i	$⊢ \{A\} \in Edg (G) \leftrightarrow \{A\} \in ran iEdg (G)$
32		elrnrexdm	$⊢ Fun iEdg (G) \to (\{A\} \in ran iEdg (G) \to \exists j \in dom iEdg (G) \{A\} = iEdg (G) (j))$
33		eqcom	$⊢ \{A\} = iEdg (G) (j) \leftrightarrow iEdg (G) (j) = \{A\}$
34	33	rexbii	$⊢ \exists j \in dom iEdg (G) \{A\} = iEdg (G) (j) \leftrightarrow \exists j \in dom iEdg (G) iEdg (G) (j) = \{A\}$
35	32 34	imbitrdi	$⊢ Fun iEdg (G) \to (\{A\} \in ran iEdg (G) \to \exists j \in dom iEdg (G) iEdg (G) (j) = \{A\})$
36	31 35	biimtrid	$⊢ Fun iEdg (G) \to (\{A\} \in Edg (G) \to \exists j \in dom iEdg (G) iEdg (G) (j) = \{A\})$
37	19 36	syl	$⊢ G \in UHGraph \to (\{A\} \in Edg (G) \to \exists j \in dom iEdg (G) iEdg (G) (j) = \{A\})$
38		df-rex	$⊢ \exists j \in dom iEdg (G) iEdg (G) (j) = \{A\} \leftrightarrow \exists j (j \in dom iEdg (G) \land iEdg (G) (j) = \{A\})$
39	37 38	imbitrdi	$⊢ G \in UHGraph \to (\{A\} \in Edg (G) \to \exists j (j \in dom iEdg (G) \land iEdg (G) (j) = \{A\}))$
40	18	lp1cycl	$⊢ (G \in UHGraph \land j \in dom iEdg (G) \land iEdg (G) (j) = \{A\}) \to ⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩$
41	40	3expib	$⊢ G \in UHGraph \to ((j \in dom iEdg (G) \land iEdg (G) (j) = \{A\}) \to ⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩)$
42	41	eximdv	$⊢ G \in UHGraph \to (\exists j (j \in dom iEdg (G) \land iEdg (G) (j) = \{A\}) \to \exists j ⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩)$
43	39 42	syld	$⊢ G \in UHGraph \to (\{A\} \in Edg (G) \to \exists j ⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩)$
44		s1len	$⊢ \|⟨“ j ”⟩\| = 1$
45	44	ax-gen	$⊢ \forall j \|⟨“ j ”⟩\| = 1$
46		19.29r	$⊢ (\exists j ⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \forall j \|⟨“ j ”⟩\| = 1) \to \exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1)$
47	45 46	mpan2	$⊢ \exists j ⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \to \exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1)$
48	43 47	syl6	$⊢ G \in UHGraph \to (\{A\} \in Edg (G) \to \exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1))$
49	48	imp	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1)$
50		uhgredgn0	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \{A\} \in (𝒫 Vtx (G) ∖ \{\emptyset\})$
51		eldifsni	$⊢ \{A\} \in (𝒫 Vtx (G) ∖ \{\emptyset\}) \to \{A\} \neq \emptyset$
52	50 51	syl	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \{A\} \neq \emptyset$
53		snnzb	$⊢ A \in V \leftrightarrow \{A\} \neq \emptyset$
54	52 53	sylibr	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to A \in V$
55		s2fv0	$⊢ A \in V \to ⟨“ A A ”⟩ (0) = A$
56	54 55	syl	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to ⟨“ A A ”⟩ (0) = A$
57	56	alrimiv	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \forall j ⟨“ A A ”⟩ (0) = A$
58		19.29r	$⊢ (\exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1) \land \forall j ⟨“ A A ”⟩ (0) = A) \to \exists j ((⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1) \land ⟨“ A A ”⟩ (0) = A)$
59	49 57 58	syl2anc	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \exists j ((⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1) \land ⟨“ A A ”⟩ (0) = A)$
60		df-3an	$⊢ (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A) \leftrightarrow ((⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1) \land ⟨“ A A ”⟩ (0) = A)$
61	60	exbii	$⊢ \exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A) \leftrightarrow \exists j ((⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1) \land ⟨“ A A ”⟩ (0) = A)$
62	59 61	sylibr	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A)$
63		s1cli	$⊢ ⟨“ j ”⟩ \in Word V$
64		breq1	$⊢ f = ⟨“ j ”⟩ \to (f Cycles (G) ⟨“ A A ”⟩ \leftrightarrow ⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩)$
65		fveqeq2	$⊢ f = ⟨“ j ”⟩ \to (\|f\| = 1 \leftrightarrow \|⟨“ j ”⟩\| = 1)$
66	64 65	3anbi12d	$⊢ f = ⟨“ j ”⟩ \to ((f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A) \leftrightarrow (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A))$
67	66	rspcev	$⊢ (⟨“ j ”⟩ \in Word V \land (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A)) \to \exists f \in Word V (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A)$
68	63 67	mpan	$⊢ (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A) \to \exists f \in Word V (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A)$
69		rexex	$⊢ \exists f \in Word V (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A) \to \exists f (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A)$
70	68 69	syl	$⊢ (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A) \to \exists f (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A)$
71	70	exlimiv	$⊢ \exists j (⟨“ j ”⟩ Cycles (G) ⟨“ A A ”⟩ \land \|⟨“ j ”⟩\| = 1 \land ⟨“ A A ”⟩ (0) = A) \to \exists f (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A)$
72	62 71	syl	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \exists f (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A)$
73		s2cli	$⊢ ⟨“ A A ”⟩ \in Word V$
74		breq2	$⊢ p = ⟨“ A A ”⟩ \to (f Cycles (G) p \leftrightarrow f Cycles (G) ⟨“ A A ”⟩)$
75		fveq1	$⊢ p = ⟨“ A A ”⟩ \to p (0) = ⟨“ A A ”⟩ (0)$
76	75	eqeq1d	$⊢ p = ⟨“ A A ”⟩ \to (p (0) = A \leftrightarrow ⟨“ A A ”⟩ (0) = A)$
77	74 76	3anbi13d	$⊢ p = ⟨“ A A ”⟩ \to ((f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \leftrightarrow (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A))$
78	77	rspcev	$⊢ (⟨“ A A ”⟩ \in Word V \land (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A)) \to \exists p \in Word V (f Cycles (G) p \land \|f\| = 1 \land p (0) = A)$
79	73 78	mpan	$⊢ (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A) \to \exists p \in Word V (f Cycles (G) p \land \|f\| = 1 \land p (0) = A)$
80		rexex	$⊢ \exists p \in Word V (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \to \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A)$
81	79 80	syl	$⊢ (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A) \to \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A)$
82	81	eximi	$⊢ \exists f (f Cycles (G) ⟨“ A A ”⟩ \land \|f\| = 1 \land ⟨“ A A ”⟩ (0) = A) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A)$
83	72 82	syl	$⊢ (G \in UHGraph \land \{A\} \in Edg (G)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A)$
84	83	ex	$⊢ G \in UHGraph \to (\{A\} \in Edg (G) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A))$
85	29 84	impbid	$⊢ G \in UHGraph \to (\exists f \exists p (f Cycles (G) p \land \|f\| = 1 \land p (0) = A) \leftrightarrow \{A\} \in Edg (G))$

Metamath Proof Explorer

Theorem loop1cycl

Proof