umgr2cycl

Description: A multigraph with two distinct edges that connect the same vertices has a 2-cycle. (Contributed by BTernaryTau, 17-Oct-2023)

		Ref	Expression
	Hypothesis	umgr2cycl.1	$⊢ I = iEdg (G)$
	Assertion	umgr2cycl	$⊢ (G \in UMGraph \land \exists j \in dom I \exists k \in dom I (I (j) = I (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2)$

Proof

Step	Hyp	Ref	Expression
1		umgr2cycl.1	$⊢ I = iEdg (G)$
2		ax-5	$⊢ j \in dom I \to \forall k j \in dom I$
3		alral	$⊢ \forall k j \in dom I \to \forall k \in dom I j \in dom I$
4	2 3	syl	$⊢ j \in dom I \to \forall k \in dom I j \in dom I$
5		r19.29	$⊢ (\forall k \in dom I j \in dom I \land \exists k \in dom I (I (j) = I (k) \land j \neq k)) \to \exists k \in dom I (j \in dom I \land (I (j) = I (k) \land j \neq k))$
6	4 5	sylan	$⊢ (j \in dom I \land \exists k \in dom I (I (j) = I (k) \land j \neq k)) \to \exists k \in dom I (j \in dom I \land (I (j) = I (k) \land j \neq k))$
7		eqid	$⊢ ⟨“ j k ”⟩ = ⟨“ j k ”⟩$
8		simp1	$⊢ (G \in UMGraph \land j \in dom I \land (I (j) = I (k) \land j \neq k)) \to G \in UMGraph$
9		simp2	$⊢ (G \in UMGraph \land j \in dom I \land (I (j) = I (k) \land j \neq k)) \to j \in dom I$
10		simp3r	$⊢ (G \in UMGraph \land j \in dom I \land (I (j) = I (k) \land j \neq k)) \to j \neq k$
11		simp3l	$⊢ (G \in UMGraph \land j \in dom I \land (I (j) = I (k) \land j \neq k)) \to I (j) = I (k)$
12	7 1 8 9 10 11	umgr2cycllem	$⊢ (G \in UMGraph \land j \in dom I \land (I (j) = I (k) \land j \neq k)) \to \exists p ⟨“ j k ”⟩ Cycles (G) p$
13		s2len	$⊢ \|⟨“ j k ”⟩\| = 2$
14	13	ax-gen	$⊢ \forall p \|⟨“ j k ”⟩\| = 2$
15		19.29r	$⊢ (\exists p ⟨“ j k ”⟩ Cycles (G) p \land \forall p \|⟨“ j k ”⟩\| = 2) \to \exists p (⟨“ j k ”⟩ Cycles (G) p \land \|⟨“ j k ”⟩\| = 2)$
16		s2cli	$⊢ ⟨“ j k ”⟩ \in Word V$
17		breq1	$⊢ f = ⟨“ j k ”⟩ \to (f Cycles (G) p \leftrightarrow ⟨“ j k ”⟩ Cycles (G) p)$
18		fveqeq2	$⊢ f = ⟨“ j k ”⟩ \to (\|f\| = 2 \leftrightarrow \|⟨“ j k ”⟩\| = 2)$
19	17 18	anbi12d	$⊢ f = ⟨“ j k ”⟩ \to ((f Cycles (G) p \land \|f\| = 2) \leftrightarrow (⟨“ j k ”⟩ Cycles (G) p \land \|⟨“ j k ”⟩\| = 2))$
20	19	rspcev	$⊢ (⟨“ j k ”⟩ \in Word V \land (⟨“ j k ”⟩ Cycles (G) p \land \|⟨“ j k ”⟩\| = 2)) \to \exists f \in Word V (f Cycles (G) p \land \|f\| = 2)$
21	16 20	mpan	$⊢ (⟨“ j k ”⟩ Cycles (G) p \land \|⟨“ j k ”⟩\| = 2) \to \exists f \in Word V (f Cycles (G) p \land \|f\| = 2)$
22		rexex	$⊢ \exists f \in Word V (f Cycles (G) p \land \|f\| = 2) \to \exists f (f Cycles (G) p \land \|f\| = 2)$
23	21 22	syl	$⊢ (⟨“ j k ”⟩ Cycles (G) p \land \|⟨“ j k ”⟩\| = 2) \to \exists f (f Cycles (G) p \land \|f\| = 2)$
24	23	eximi	$⊢ \exists p (⟨“ j k ”⟩ Cycles (G) p \land \|⟨“ j k ”⟩\| = 2) \to \exists p \exists f (f Cycles (G) p \land \|f\| = 2)$
25		excomim	$⊢ \exists p \exists f (f Cycles (G) p \land \|f\| = 2) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2)$
26	15 24 25	3syl	$⊢ (\exists p ⟨“ j k ”⟩ Cycles (G) p \land \forall p \|⟨“ j k ”⟩\| = 2) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2)$
27	12 14 26	sylancl	$⊢ (G \in UMGraph \land j \in dom I \land (I (j) = I (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2)$
28	27	3expib	$⊢ G \in UMGraph \to ((j \in dom I \land (I (j) = I (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2))$
29	28	rexlimdvw	$⊢ G \in UMGraph \to (\exists k \in dom I (j \in dom I \land (I (j) = I (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2))$
30	6 29	syl5	$⊢ G \in UMGraph \to ((j \in dom I \land \exists k \in dom I (I (j) = I (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2))$
31	30	expd	$⊢ G \in UMGraph \to (j \in dom I \to (\exists k \in dom I (I (j) = I (k) \land j \neq k) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2)))$
32	31	rexlimdv	$⊢ G \in UMGraph \to (\exists j \in dom I \exists k \in dom I (I (j) = I (k) \land j \neq k) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2))$
33	32	imp	$⊢ (G \in UMGraph \land \exists j \in dom I \exists k \in dom I (I (j) = I (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2)$

Metamath Proof Explorer

Theorem umgr2cycl

Proof