Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  usgra2pth Unicode version

Theorem usgra2pth 28669
Description: In a undirected simply graph, there is a path of length 2 if and only if there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.)
Assertion
Ref Expression
usgra2pth
Distinct variable groups:   , , ,   , , ,   ,P, ,   , , ,

Proof of Theorem usgra2pth
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 usgra2pthspth 28663 . . . . . . 7
2 spthispth 21609 . . . . . . . . . 10
3 pthistrl 21608 . . . . . . . . . 10
4 trliswlk 21575 . . . . . . . . . . 11
5 wlkbprop 21570 . . . . . . . . . . 11
6 3simpc 957 . . . . . . . . . . 11
74, 5, 63syl 19 . . . . . . . . . 10
82, 3, 73syl 19 . . . . . . . . 9
9 isspth 21605 . . . . . . . . . 10
10 istrl2 21574 . . . . . . . . . . . 12
1110anbi1d 687 . . . . . . . . . . 11
12 oveq2 6141 . . . . . . . . . . . . . . . . . . . 20
13 f1eq2 5686 . . . . . . . . . . . . . . . . . . . 20
1412, 13syl 16 . . . . . . . . . . . . . . . . . . 19
1514biimpd 200 . . . . . . . . . . . . . . . . . 18
1615adantl 454 . . . . . . . . . . . . . . . . 17
1716com12 30 . . . . . . . . . . . . . . . 16
18173ad2ant1 979 . . . . . . . . . . . . . . 15
1918adantr 453 . . . . . . . . . . . . . 14
2019adantl 454 . . . . . . . . . . . . 13
21 oveq2 6141 . . . . . . . . . . . . . . . . . . . 20
2221feq2d 5632 . . . . . . . . . . . . . . . . . . 19
23 df-f1 5510 . . . . . . . . . . . . . . . . . . . . 21
2423simplbi2 610 . . . . . . . . . . . . . . . . . . . 20
2524a1i 11 . . . . . . . . . . . . . . . . . . 19
2622, 25sylbid 208 . . . . . . . . . . . . . . . . . 18
2726adantl 454 . . . . . . . . . . . . . . . . 17
2827com3l 78 . . . . . . . . . . . . . . . 16
29283ad2ant2 980 . . . . . . . . . . . . . . 15
3029imp 420 . . . . . . . . . . . . . 14
3130adantl 454 . . . . . . . . . . . . 13
32 usgra2pthlem1 28668 . . . . . . . . . . . . . . 15
3332adantr 453 . . . . . . . . . . . . . 14
3433adantl 454 . . . . . . . . . . . . 13
3520, 31, 343jcad 1136 . . . . . . . . . . . 12
3635ex 425 . . . . . . . . . . 11
3711, 36sylbid 208 . . . . . . . . . 10
389, 37sylbid 208 . . . . . . . . 9
398, 38mpcom 35 . . . . . . . 8
4039com12 30 . . . . . . 7
411, 40sylbid 208 . . . . . 6
4241ex 425 . . . . 5
4342com13 77 . . . 4
4443imp 420 . . 3
4544com12 30 . 2
46 2nn0 10293 . . . . . 6
47 f1f 5690 . . . . . 6
48 hashfirdm 28508 . . . . . 6
4946, 47, 48sylancr 646 . . . . 5
50 oveq2 6141 . . . . . . . . . . . . . . . . . . . 20
5150eqcoms 2450 . . . . . . . . . . . . . . . . . . 19
52 f1eq2 5686 . . . . . . . . . . . . . . . . . . 19
5351, 52syl 16 . . . . . . . . . . . . . . . . . 18
5453biimpd 200 . . . . . . . . . . . . . . . . 17
5554imp 420 . . . . . . . . . . . . . . . 16
5655adantr 453 . . . . . . . . . . . . . . 15
5756ad2antrr 708 . . . . . . . . . . . . . 14
58 f1f 5690 . . . . . . . . . . . . . . . . 17
59 oveq2 6141 . . . . . . . . . . . . . . . . . . . 20
6059eqcoms 2450 . . . . . . . . . . . . . . . . . . 19
6160adantr 453 . . . . . . . . . . . . . . . . . 18
6261feq2d 5632 . . . . . . . . . . . . . . . . 17
6358, 62syl5ib 212 . . . . . . . . . . . . . . . 16
6463imp 420 . . . . . . . . . . . . . . 15
6564ad2antrr 708 . . . . . . . . . . . . . 14
66 eqcom 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6766biimpi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
68673ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
69 eqcom 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7069biimpi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
71703ad2ant2 980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7268, 71preq12d 3923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7372eqeq2d 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7473biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7574com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7675adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25
7776impcom 421 . . . . . . . . . . . . . . . . . . . . . . . 24
78 eqcom 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7978biimpi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
80793ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8171, 80preq12d 3923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8281eqeq2d 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8382biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8483com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8584adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . 25
8685impcom 421 . . . . . . . . . . . . . . . . . . . . . . . 24
8777, 86jca 520 . . . . . . . . . . . . . . . . . . . . . . 23
8887rexlimivw 2837 . . . . . . . . . . . . . . . . . . . . . 22
8988rexlimivw 2837 . . . . . . . . . . . . . . . . . . . . 21
9089rexlimivw 2837 . . . . . . . . . . . . . . . . . . . 20
9190a1d 24 . . . . . . . . . . . . . . . . . . 19
9291a1i 11 . . . . . . . . . . . . . . . . . 18
93 fzo0to2pr 11239 . . . . . . . . . . . . . . . . . . . . . . 23
9412, 93syl6eq 2495 . . . . . . . . . . . . . . . . . . . . . 22
9594raleqdv 2921 . . . . . . . . . . . . . . . . . . . . 21
96 c0ex 9140 . . . . . . . . . . . . . . . . . . . . . . 23
97 1ex 9141 . . . . . . . . . . . . . . . . . . . . . . 23
98 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9998fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . 25
100 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . . . . . 26
101 oveq1 6140 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102 0p1e1 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103101, 102syl6eq 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
104103fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . . 26
105100, 104preq12d 3923 . . . . . . . . . . . . . . . . . . . . . . . . 25
10699, 105eqeq12d 2461 . . . . . . . . . . . . . . . . . . . . . . . 24
107 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . . . . . 26
108107fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . 25
109 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . . . . . 26
110 oveq1 6140 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111 1p1e2 10149 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
112110, 111syl6eq 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
113112fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . . 26
114109, 113preq12d 3923 . . . . . . . . . . . . . . . . . . . . . . . . 25
115108, 114eqeq12d 2461 . . . . . . . . . . . . . . . . . . . . . . . 24
116106, 115ralprg 3889 . . . . . . . . . . . . . . . . . . . . . . 23
11796, 97, 116mp2an 655 . . . . . . . . . . . . . . . . . . . . . 22
118117a1i 11 . . . . . . . . . . . . . . . . . . . . 21
11995, 118bitrd 246 . . . . . . . . . . . . . . . . . . . 20
120119imbi2d 309 . . . . . . . . . . . . . . . . . . 19
121120imbi2d 309 . . . . . . . . . . . . . . . . . 18
12292, 121mpbird 225 . . . . . . . . . . . . . . . . 17
123122ad2antrr 708 . . . . . . . . . . . . . . . 16
124123imp 420 . . . . . . . . . . . . . . 15