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 e. UPGraph /\ F ( Paths ` G ) P /\ 1 < ( # ` F ) ) -> A. i e. ( 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 ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) )
3 2 3adant1 
 |-  ( ( G e. UPGraph /\ F ( Paths ` G ) P /\ 1 < ( # ` F ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) )
4 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
5 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
6 simp2 
 |-  ( ( F e. Word dom I /\ G e. UPGraph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> G e. UPGraph )
7 wrdsymbcl 
 |-  ( ( F e. Word dom I /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` i ) e. dom I )
8 1 upgrle2 
 |-  ( ( G e. UPGraph /\ ( F ` i ) e. dom I ) -> ( # ` ( I ` ( F ` i ) ) ) <_ 2 )
9 6 7 8 3imp3i2an 
 |-  ( ( F e. Word dom I /\ G e. UPGraph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) <_ 2 )
10 fvex 
 |-  ( I ` ( F ` i ) ) e. _V
11 hashxnn0 
 |-  ( ( I ` ( F ` i ) ) e. _V -> ( # ` ( I ` ( F ` i ) ) ) e. NN0* )
12 xnn0xr 
 |-  ( ( # ` ( I ` ( F ` i ) ) ) e. NN0* -> ( # ` ( I ` ( F ` i ) ) ) e. RR* )
13 10 11 12 mp2b 
 |-  ( # ` ( I ` ( F ` i ) ) ) e. RR*
14 2re 
 |-  2 e. RR
15 14 rexri 
 |-  2 e. RR*
16 13 15 pm3.2i 
 |-  ( ( # ` ( I ` ( F ` i ) ) ) e. RR* /\ 2 e. RR* )
17 xrletri3 
 |-  ( ( ( # ` ( I ` ( F ` i ) ) ) e. RR* /\ 2 e. RR* ) -> ( ( # ` ( I ` ( F ` i ) ) ) = 2 <-> ( ( # ` ( I ` ( F ` i ) ) ) <_ 2 /\ 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) )
18 16 17 mp1i 
 |-  ( ( F e. Word dom I /\ G e. UPGraph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( # ` ( I ` ( F ` i ) ) ) = 2 <-> ( ( # ` ( I ` ( F ` i ) ) ) <_ 2 /\ 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) )
19 18 biimprd 
 |-  ( ( F e. Word dom I /\ G e. UPGraph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( # ` ( I ` ( F ` i ) ) ) <_ 2 /\ 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) = 2 ) )
20 9 19 mpand 
 |-  ( ( F e. Word dom I /\ G e. UPGraph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( 2 <_ ( # ` ( I ` ( F ` i ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) = 2 ) )
21 20 3exp 
 |-  ( F e. Word dom I -> ( G e. UPGraph -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( 2 <_ ( # ` ( I ` ( F ` i ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) = 2 ) ) ) )
22 4 5 21 3syl 
 |-  ( F ( Paths ` G ) P -> ( G e. UPGraph -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( 2 <_ ( # ` ( I ` ( F ` i ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) = 2 ) ) ) )
23 22 impcom 
 |-  ( ( G e. UPGraph /\ F ( Paths ` G ) P ) -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( 2 <_ ( # ` ( I ` ( F ` i ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) = 2 ) ) )
24 23 3adant3 
 |-  ( ( G e. UPGraph /\ F ( Paths ` G ) P /\ 1 < ( # ` F ) ) -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( 2 <_ ( # ` ( I ` ( F ` i ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) = 2 ) ) )
25 24 imp 
 |-  ( ( ( G e. UPGraph /\ F ( Paths ` G ) P /\ 1 < ( # ` F ) ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( 2 <_ ( # ` ( I ` ( F ` i ) ) ) -> ( # ` ( I ` ( F ` i ) ) ) = 2 ) )
26 25 ralimdva 
 |-  ( ( G e. UPGraph /\ F ( Paths ` G ) P /\ 1 < ( # ` F ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) ( # ` ( I ` ( F ` i ) ) ) = 2 ) )
27 3 26 mpd 
 |-  ( ( G e. UPGraph /\ F ( Paths ` G ) P /\ 1 < ( # ` F ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) ( # ` ( I ` ( F ` i ) ) ) = 2 )