Metamath Proof Explorer

Theorem upgr2pthnlp

Description: A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021)

Ref Expression
Hypothesis 2pthnloop.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion upgr2pthnlp ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 )

Proof

Step Hyp Ref Expression
1 2pthnloop.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 1 2pthnloop ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
3 2 3adant1 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
4 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
5 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
6 simp2 ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝐺 ∈ UPGraph ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐺 ∈ UPGraph )
7 wrdsymbcl ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐼 )
8 1 upgrle2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ‘ 𝑖 ) ∈ dom 𝐼 ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ≤ 2 )
9 6 7 8 3imp3i2an ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝐺 ∈ UPGraph ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ≤ 2 )
10 fvex ⊢ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ V
11 hashxnn0 ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ V → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℕ0* )
12 xnn0xr ⊢ ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℕ0* → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℝ* )
13 10 11 12 mp2b ⊢ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℝ*
14 2re ⊢ 2 ∈ ℝ
15 14 rexri ⊢ 2 ∈ ℝ*
16 13 15 pm3.2i ⊢ ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℝ* ∧ 2 ∈ ℝ* )
17 xrletri3 ⊢ ( ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℝ* ∧ 2 ∈ ℝ* ) → ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ↔ ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) ) )
18 16 17 mp1i ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝐺 ∈ UPGraph ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ↔ ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) ) )
19 18 biimprd ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝐺 ∈ UPGraph ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) )
20 9 19 mpand ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝐺 ∈ UPGraph ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) )
21 20 3exp ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝐺 ∈ UPGraph → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) ) ) )
22 4 5 21 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) ) ) )
23 22 impcom ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) ) )
24 23 3adant3 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) ) )
25 24 imp ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) )
26 25 ralimdva ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 2 ≤ ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 ) )
27 3 26 mpd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ 1 < ( ♯ ‘ 𝐹 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ♯ ‘ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = 2 )