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	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	Assertion	umgr2cycl	⊢ ( ( 𝐺 ∈ UMGraph ∧ ∃ 𝑗 ∈ dom 𝐼 ∃ 𝑘 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )

Proof

Step	Hyp	Ref	Expression
1		umgr2cycl.1	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		ax-5	⊢ ( 𝑗 ∈ dom 𝐼 → ∀ 𝑘 𝑗 ∈ dom 𝐼 )
3		alral	⊢ ( ∀ 𝑘 𝑗 ∈ dom 𝐼 → ∀ 𝑘 ∈ dom 𝐼 𝑗 ∈ dom 𝐼 )
4	2 3	syl	⊢ ( 𝑗 ∈ dom 𝐼 → ∀ 𝑘 ∈ dom 𝐼 𝑗 ∈ dom 𝐼 )
5		r19.29	⊢ ( ( ∀ 𝑘 ∈ dom 𝐼 𝑗 ∈ dom 𝐼 ∧ ∃ 𝑘 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑘 ∈ dom 𝐼 ( 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) )
6	4 5	sylan	⊢ ( ( 𝑗 ∈ dom 𝐼 ∧ ∃ 𝑘 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑘 ∈ dom 𝐼 ( 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) )
7		eqid	⊢ ⟨“ 𝑗 𝑘 ”⟩ = ⟨“ 𝑗 𝑘 ”⟩
8		simp1	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → 𝐺 ∈ UMGraph )
9		simp2	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → 𝑗 ∈ dom 𝐼 )
10		simp3r	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → 𝑗 ≠ 𝑘 )
11		simp3l	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) )
12	7 1 8 9 10 11	umgr2cycllem	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑝 ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 )
13		s2len	⊢ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2
14	13	ax-gen	⊢ ∀ 𝑝 ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2
15		19.29r	⊢ ( ( ∃ 𝑝 ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ∀ 𝑝 ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) → ∃ 𝑝 ( ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) )
16		s2cli	⊢ ⟨“ 𝑗 𝑘 ”⟩ ∈ Word V
17		breq1	⊢ ( 𝑓 = ⟨“ 𝑗 𝑘 ”⟩ → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ↔ ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ) )
18		fveqeq2	⊢ ( 𝑓 = ⟨“ 𝑗 𝑘 ”⟩ → ( ( ♯ ‘ 𝑓 ) = 2 ↔ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) )
19	17 18	anbi12d	⊢ ( 𝑓 = ⟨“ 𝑗 𝑘 ”⟩ → ( ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ ( ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) ) )
20	19	rspcev	⊢ ( ( ⟨“ 𝑗 𝑘 ”⟩ ∈ Word V ∧ ( ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) ) → ∃ 𝑓 ∈ Word V ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
21	16 20	mpan	⊢ ( ( ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) → ∃ 𝑓 ∈ Word V ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
22		rexex	⊢ ( ∃ 𝑓 ∈ Word V ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
23	21 22	syl	⊢ ( ( ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) → ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
24	23	eximi	⊢ ( ∃ 𝑝 ( ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) → ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
25		excomim	⊢ ( ∃ 𝑝 ∃ 𝑓 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
26	15 24 25	3syl	⊢ ( ( ∃ 𝑝 ⟨“ 𝑗 𝑘 ”⟩ ( Cycles ‘ 𝐺 ) 𝑝 ∧ ∀ 𝑝 ( ♯ ‘ ⟨“ 𝑗 𝑘 ”⟩ ) = 2 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
27	12 14 26	sylancl	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
28	27	3expib	⊢ ( 𝐺 ∈ UMGraph → ( ( 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
29	28	rexlimdvw	⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑘 ∈ dom 𝐼 ( 𝑗 ∈ dom 𝐼 ∧ ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
30	6 29	syl5	⊢ ( 𝐺 ∈ UMGraph → ( ( 𝑗 ∈ dom 𝐼 ∧ ∃ 𝑘 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
31	30	expd	⊢ ( 𝐺 ∈ UMGraph → ( 𝑗 ∈ dom 𝐼 → ( ∃ 𝑘 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) ) )
32	31	rexlimdv	⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑗 ∈ dom 𝐼 ∃ 𝑘 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
33	32	imp	⊢ ( ( 𝐺 ∈ UMGraph ∧ ∃ 𝑗 ∈ dom 𝐼 ∃ 𝑘 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑗 ) = ( 𝐼 ‘ 𝑘 ) ∧ 𝑗 ≠ 𝑘 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )

Metamath Proof Explorer

Theorem umgr2cycl

Proof