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 F Paths G P 1 < F i 0 ..^ F I F i = 2

Proof

Step Hyp Ref Expression
1 2pthnloop.i I = iEdg G
2 1 2pthnloop F Paths G P 1 < F i 0 ..^ F 2 I F i
3 2 3adant1 G UPGraph F Paths G P 1 < F i 0 ..^ F 2 I F i
4 pthiswlk F Paths G P F Walks G P
5 1 wlkf F Walks G P F Word dom I
6 simp2 F Word dom I G UPGraph i 0 ..^ F G UPGraph
7 wrdsymbcl F Word dom 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 Word dom 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 Word dom I G UPGraph i 0 ..^ F I F i = 2 I F i 2 2 I F i
19 18 biimprd F Word dom I G UPGraph i 0 ..^ F I F i 2 2 I F i I F i = 2
20 9 19 mpand F Word dom I G UPGraph i 0 ..^ F 2 I F i I F i = 2
21 20 3exp F Word dom I G UPGraph i 0 ..^ F 2 I F i I F i = 2
22 4 5 21 3syl F Paths G P G UPGraph i 0 ..^ F 2 I F i I F i = 2
23 22 impcom G UPGraph F Paths G P i 0 ..^ F 2 I F i I F i = 2
24 23 3adant3 G UPGraph F Paths G P 1 < F i 0 ..^ F 2 I F i I F i = 2
25 24 imp G UPGraph F Paths G P 1 < F i 0 ..^ F 2 I F i I F i = 2
26 25 ralimdva G UPGraph F Paths G P 1 < F i 0 ..^ F 2 I F i i 0 ..^ F I F i = 2
27 3 26 mpd G UPGraph F Paths G P 1 < F i 0 ..^ F I F i = 2