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 ⊢I=iEdg⁡G
Assertion upgr2pthnlp ⊢G∈UPGraph∧FPaths⁡GP∧1<F→∀i∈0..^FI⁡F⁡i=2

Proof

Step Hyp Ref Expression
1 2pthnloop.i ⊢I=iEdg⁡G
2 1 2pthnloop ⊢FPaths⁡GP∧1<F→∀i∈0..^F2≤I⁡F⁡i
3 2 3adant1 ⊢G∈UPGraph∧FPaths⁡GP∧1<F→∀i∈0..^F2≤I⁡F⁡i
4 pthiswlk ⊢FPaths⁡GP→FWalks⁡GP
5 1 wlkf ⊢FWalks⁡GP→F∈Worddom⁡I
6 simp2 ⊢F∈Worddom⁡I∧G∈UPGraph∧i∈0..^F→G∈UPGraph
7 wrdsymbcl ⊢F∈Worddom⁡I∧i∈0..^F→F⁡i∈dom⁡I
8 1 upgrle2 ⊢G∈UPGraph∧F⁡i∈dom⁡I→I⁡F⁡i≤2
9 6 7 8 3imp3i2an ⊢F∈Worddom⁡I∧G∈UPGraph∧i∈0..^F→I⁡F⁡i≤2
10 fvex ⊢I⁡F⁡i∈V
11 hashxnn0 ⊢I⁡F⁡i∈V→I⁡F⁡i∈ℕ0*
12 xnn0xr ⊢I⁡F⁡i∈ℕ0*→I⁡F⁡i∈ℝ*
13 10 11 12 mp2b ⊢I⁡F⁡i∈ℝ*
14 2re ⊢2∈ℝ
15 14 rexri ⊢2∈ℝ*
16 13 15 pm3.2i ⊢I⁡F⁡i∈ℝ*∧2∈ℝ*
17 xrletri3 ⊢I⁡F⁡i∈ℝ*∧2∈ℝ*→I⁡F⁡i=2↔I⁡F⁡i≤2∧2≤I⁡F⁡i
18 16 17 mp1i ⊢F∈Worddom⁡I∧G∈UPGraph∧i∈0..^F→I⁡F⁡i=2↔I⁡F⁡i≤2∧2≤I⁡F⁡i
19 18 biimprd ⊢F∈Worddom⁡I∧G∈UPGraph∧i∈0..^F→I⁡F⁡i≤2∧2≤I⁡F⁡i→I⁡F⁡i=2
20 9 19 mpand ⊢F∈Worddom⁡I∧G∈UPGraph∧i∈0..^F→2≤I⁡F⁡i→I⁡F⁡i=2
21 20 3exp ⊢F∈Worddom⁡I→G∈UPGraph→i∈0..^F→2≤I⁡F⁡i→I⁡F⁡i=2
22 4 5 21 3syl ⊢FPaths⁡GP→G∈UPGraph→i∈0..^F→2≤I⁡F⁡i→I⁡F⁡i=2
23 22 impcom ⊢G∈UPGraph∧FPaths⁡GP→i∈0..^F→2≤I⁡F⁡i→I⁡F⁡i=2
24 23 3adant3 ⊢G∈UPGraph∧FPaths⁡GP∧1<F→i∈0..^F→2≤I⁡F⁡i→I⁡F⁡i=2
25 24 imp ⊢G∈UPGraph∧FPaths⁡GP∧1<F∧i∈0..^F→2≤I⁡F⁡i→I⁡F⁡i=2
26 25 ralimdva ⊢G∈UPGraph∧FPaths⁡GP∧1<F→∀i∈0..^F2≤I⁡F⁡i→∀i∈0..^FI⁡F⁡i=2
27 3 26 mpd ⊢G∈UPGraph∧FPaths⁡GP∧1<F→∀i∈0..^FI⁡F⁡i=2