Metamath Proof Explorer

Theorem umgr2cycllem

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

Ref Expression
Hypotheses umgr2cycllem.1 ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
umgr2cycllem.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
umgr2cycllem.3 ⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
umgr2cycllem.4 ⊢ ( 𝜑 → 𝐽 ∈ dom 𝐼 )
umgr2cycllem.5 ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
umgr2cycllem.6 ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) = ( 𝐼 ‘ 𝐾 ) )
Assertion umgr2cycllem ( 𝜑 → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )

Proof

Step Hyp Ref Expression
1 umgr2cycllem.1 ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2 umgr2cycllem.2 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 umgr2cycllem.3 ⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
4 umgr2cycllem.4 ⊢ ( 𝜑 → 𝐽 ∈ dom 𝐼 )
5 umgr2cycllem.5 ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
6 umgr2cycllem.6 ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) = ( 𝐼 ‘ 𝐾 ) )
7 umgruhgr ⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
8 2 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
9 3 7 8 3syl ⊢ ( 𝜑 → Fun 𝐼 )
10 2 iedgedg ⊢ ( ( Fun 𝐼 ∧ 𝐽 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝐽 ) ∈ ( Edg ‘ 𝐺 ) )
11 9 4 10 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) ∈ ( Edg ‘ 𝐺 ) )
12 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
13 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
14 12 13 umgredg ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐼 ‘ 𝐽 ) ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) )
15 3 11 14 syl2anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) )
16 ax-5 ⊢ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ∀ 𝑏 𝑎 ∈ ( Vtx ‘ 𝐺 ) )
17 alral ⊢ ( ∀ 𝑏 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ∀ 𝑏 ∈ ( Vtx ‘ 𝐺 ) 𝑎 ∈ ( Vtx ‘ 𝐺 ) )
18 16 17 syl ⊢ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ∀ 𝑏 ∈ ( Vtx ‘ 𝐺 ) 𝑎 ∈ ( Vtx ‘ 𝐺 ) )
19 r19.29 ⊢ ( ( ∀ 𝑏 ∈ ( Vtx ‘ 𝐺 ) 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) )
20 18 19 sylan ⊢ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) )
21 eqid ⊢ ⟨“ 𝑎 𝑏 𝑎 ”⟩ = ⟨“ 𝑎 𝑏 𝑎 ”⟩
22 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝑎 ∈ ( Vtx ‘ 𝐺 ) )
23 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
24 22 23 22 3jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ) )
25 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝑎 ≠ 𝑏 )
26 25 necomd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝑏 ≠ 𝑎 )
27 25 26 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑎 ) )
28 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } )
29 28 eqimsscd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐽 ) )
30 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( 𝐼 ‘ 𝐽 ) = ( 𝐼 ‘ 𝐾 ) )
31 30 28 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( 𝐼 ‘ 𝐾 ) = { 𝑎 , 𝑏 } )
32 prcom ⊢ { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 }
33 32 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 } )
34 31 33 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( 𝐼 ‘ 𝐾 ) = { 𝑏 , 𝑎 } )
35 eqimss2 ⊢ ( ( 𝐼 ‘ 𝐾 ) = { 𝑏 , 𝑎 } → { 𝑏 , 𝑎 } ⊆ ( 𝐼 ‘ 𝐾 ) )
36 34 35 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → { 𝑏 , 𝑎 } ⊆ ( 𝐼 ‘ 𝐾 ) )
37 29 36 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝑏 , 𝑎 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
38 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐽 ≠ 𝐾 )
39 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝑎 = 𝑎 )
40 21 1 24 27 37 12 2 38 39 2cycld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ )
41 40 3expib ⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) )
42 41 exp4c ⊢ ( 𝜑 → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) ) ) )
43 42 com23 ⊢ ( 𝜑 → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) ) ) )
44 43 imp4a ⊢ ( 𝜑 → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) ) )
45 s3cli ⊢ ⟨“ 𝑎 𝑏 𝑎 ”⟩ ∈ Word V
46 breq2 ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑎 ”⟩ → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ↔ 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) )
47 46 rspcev ⊢ ( ( ⟨“ 𝑎 𝑏 𝑎 ”⟩ ∈ Word V ∧ 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) → ∃ 𝑝 ∈ Word V 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
48 45 47 mpan ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ → ∃ 𝑝 ∈ Word V 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
49 rexex ⊢ ( ∃ 𝑝 ∈ Word V 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
50 48 49 syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
51 44 50 syl8 ⊢ ( 𝜑 → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) ) )
52 51 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) )
53 20 52 syl5 ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) )
54 53 expd ⊢ ( 𝜑 → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ( ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) ) )
55 54 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) )
56 15 55 mpd ⊢ ( 𝜑 → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )