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 simp2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) )
23 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝑎 ≠ 𝑏 )
24 eqimss2 ⊢ ( ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐽 ) )
25 24 adantl ⊢ ( ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐽 ) )
26 25 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐽 ) )
27 6 sseq2d ⊢ ( 𝜑 → ( { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐽 ) ↔ { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
28 24 27 syl5ib ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
29 28 adantld ⊢ ( 𝜑 → ( ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
30 29 adantld ⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
31 30 3impib ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐾 ) )
32 26 31 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ( { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝑎 , 𝑏 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
33 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐽 ≠ 𝐾 )
34 21 1 22 23 32 12 2 33 2cycl2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ )
35 34 3expib ⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) )
36 35 exp4c ⊢ ( 𝜑 → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) ) ) )
37 36 com23 ⊢ ( 𝜑 → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) ) ) )
38 37 imp4a ⊢ ( 𝜑 → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) ) )
39 s3cli ⊢ ⟨“ 𝑎 𝑏 𝑎 ”⟩ ∈ Word V
40 breq2 ⊢ ( 𝑝 = ⟨“ 𝑎 𝑏 𝑎 ”⟩ → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ↔ 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) )
41 40 rspcev ⊢ ( ( ⟨“ 𝑎 𝑏 𝑎 ”⟩ ∈ Word V ∧ 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ ) → ∃ 𝑝 ∈ Word V 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
42 39 41 mpan ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ → ∃ 𝑝 ∈ Word V 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
43 rexex ⊢ ( ∃ 𝑝 ∈ Word V 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
44 42 43 syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) ⟨“ 𝑎 𝑏 𝑎 ”⟩ → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )
45 38 44 syl8 ⊢ ( 𝜑 → ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) ) )
46 45 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) )
47 20 46 syl5 ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) )
48 47 expd ⊢ ( 𝜑 → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ( ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) ) )
49 48 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ( 𝑎 ≠ 𝑏 ∧ ( 𝐼 ‘ 𝐽 ) = { 𝑎 , 𝑏 } ) → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 ) )
50 15 49 mpd ⊢ ( 𝜑 → ∃ 𝑝 𝐹 ( Cycles ‘ 𝐺 ) 𝑝 )