Metamath Proof Explorer

Theorem umgr2cycllem

Description: Lemma for umgr2cycl . (Contributed by BTernaryTau, 17-Oct-2023)

Ref Expression
Hypotheses umgr2cycllem.1 ⊢ F = ⟨“ JK ”⟩
umgr2cycllem.2 ⊢ I = iEdg ⁡ G
umgr2cycllem.3 ⊢ φ → G ∈ UMGraph
umgr2cycllem.4 ⊢ φ → J ∈ dom ⁡ I
umgr2cycllem.5 ⊢ φ → J ≠ K
umgr2cycllem.6 ⊢ φ → I ⁡ J = I ⁡ K
Assertion umgr2cycllem ⊢ φ → ∃ p F Cycles ⁡ G p

Proof

Step Hyp Ref Expression
1 umgr2cycllem.1 ⊢ F = ⟨“ JK ”⟩
2 umgr2cycllem.2 ⊢ I = iEdg ⁡ G
3 umgr2cycllem.3 ⊢ φ → G ∈ UMGraph
4 umgr2cycllem.4 ⊢ φ → J ∈ dom ⁡ I
5 umgr2cycllem.5 ⊢ φ → J ≠ K
6 umgr2cycllem.6 ⊢ φ → I ⁡ J = I ⁡ K
7 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
8 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
9 3 7 8 3syl ⊢ φ → Fun ⁡ I
10 2 iedgedg ⊢ Fun ⁡ I ∧ J ∈ dom ⁡ I → I ⁡ J ∈ Edg ⁡ G
11 9 4 10 syl2anc ⊢ φ → I ⁡ J ∈ Edg ⁡ G
12 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
13 eqid ⊢ Edg ⁡ G = Edg ⁡ G
14 12 13 umgredg ⊢ G ∈ UMGraph ∧ I ⁡ J ∈ Edg ⁡ G → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G a ≠ b ∧ I ⁡ J = a b
15 3 11 14 syl2anc ⊢ φ → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G a ≠ b ∧ I ⁡ J = a b
16 ax-5 ⊢ a ∈ Vtx ⁡ G → ∀ b a ∈ Vtx ⁡ G
17 alral ⊢ ∀ b a ∈ Vtx ⁡ G → ∀ b ∈ Vtx ⁡ G a ∈ Vtx ⁡ G
18 16 17 syl ⊢ a ∈ Vtx ⁡ G → ∀ b ∈ Vtx ⁡ G a ∈ Vtx ⁡ G
19 r19.29 ⊢ ∀ b ∈ Vtx ⁡ G a ∈ Vtx ⁡ G ∧ ∃ b ∈ Vtx ⁡ G a ≠ b ∧ I ⁡ J = a b → ∃ b ∈ Vtx ⁡ G a ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b
20 18 19 sylan ⊢ a ∈ Vtx ⁡ G ∧ ∃ b ∈ Vtx ⁡ G a ≠ b ∧ I ⁡ J = a b → ∃ b ∈ Vtx ⁡ G a ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b
21 eqid ⊢ ⟨“ aba ”⟩ = ⟨“ aba ”⟩
22 simp2 ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G
23 simp3l ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → a ≠ b
24 eqimss2 ⊢ I ⁡ J = a b → a b ⊆ I ⁡ J
25 24 adantl ⊢ a ≠ b ∧ I ⁡ J = a b → a b ⊆ I ⁡ J
26 25 3ad2ant3 ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → a b ⊆ I ⁡ J
27 6 sseq2d ⊢ φ → a b ⊆ I ⁡ J ↔ a b ⊆ I ⁡ K
28 24 27 syl5ib ⊢ φ → I ⁡ J = a b → a b ⊆ I ⁡ K
29 28 adantld ⊢ φ → a ≠ b ∧ I ⁡ J = a b → a b ⊆ I ⁡ K
30 29 adantld ⊢ φ → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → a b ⊆ I ⁡ K
31 30 3impib ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → a b ⊆ I ⁡ K
32 26 31 jca ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → a b ⊆ I ⁡ J ∧ a b ⊆ I ⁡ K
33 5 3ad2ant1 ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → J ≠ K
34 21 1 22 23 32 12 2 33 2cycl2d ⊢ φ ∧ a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → F Cycles ⁡ G ⟨“ aba ”⟩
35 34 3expib ⊢ φ → a ∈ Vtx ⁡ G ∧ b ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → F Cycles ⁡ G ⟨“ aba ”⟩
36 35 exp4c ⊢ φ → a ∈ Vtx ⁡ G → b ∈ Vtx ⁡ G → a ≠ b ∧ I ⁡ J = a b → F Cycles ⁡ G ⟨“ aba ”⟩
37 36 com23 ⊢ φ → b ∈ Vtx ⁡ G → a ∈ Vtx ⁡ G → a ≠ b ∧ I ⁡ J = a b → F Cycles ⁡ G ⟨“ aba ”⟩
38 37 imp4a ⊢ φ → b ∈ Vtx ⁡ G → a ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → F Cycles ⁡ G ⟨“ aba ”⟩
39 s3cli ⊢ ⟨“ aba ”⟩ ∈ Word V
40 breq2 ⊢ p = ⟨“ aba ”⟩ → F Cycles ⁡ G p ↔ F Cycles ⁡ G ⟨“ aba ”⟩
41 40 rspcev ⊢ ⟨“ aba ”⟩ ∈ Word V ∧ F Cycles ⁡ G ⟨“ aba ”⟩ → ∃ p ∈ Word V F Cycles ⁡ G p
42 39 41 mpan ⊢ F Cycles ⁡ G ⟨“ aba ”⟩ → ∃ p ∈ Word V F Cycles ⁡ G p
43 rexex ⊢ ∃ p ∈ Word V F Cycles ⁡ G p → ∃ p F Cycles ⁡ G p
44 42 43 syl ⊢ F Cycles ⁡ G ⟨“ aba ”⟩ → ∃ p F Cycles ⁡ G p
45 38 44 syl8 ⊢ φ → b ∈ Vtx ⁡ G → a ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → ∃ p F Cycles ⁡ G p
46 45 rexlimdv ⊢ φ → ∃ b ∈ Vtx ⁡ G a ∈ Vtx ⁡ G ∧ a ≠ b ∧ I ⁡ J = a b → ∃ p F Cycles ⁡ G p
47 20 46 syl5 ⊢ φ → a ∈ Vtx ⁡ G ∧ ∃ b ∈ Vtx ⁡ G a ≠ b ∧ I ⁡ J = a b → ∃ p F Cycles ⁡ G p
48 47 expd ⊢ φ → a ∈ Vtx ⁡ G → ∃ b ∈ Vtx ⁡ G a ≠ b ∧ I ⁡ J = a b → ∃ p F Cycles ⁡ G p
49 48 rexlimdv ⊢ φ → ∃ a ∈ Vtx ⁡ G ∃ b ∈ Vtx ⁡ G a ≠ b ∧ I ⁡ J = a b → ∃ p F Cycles ⁡ G p
50 15 49 mpd ⊢ φ → ∃ p F Cycles ⁡ G p