Metamath Proof Explorer


Theorem usgr2pth0

Description: In a simply graph, there is a path of length 2 iff 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) (Revised by AV, 5-Jun-2021)

Ref Expression
Hypotheses usgr2pthlem.v V = Vtx G
usgr2pthlem.i I = iEdg G
Assertion usgr2pth0 G USGraph F Paths G P F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y

Proof

Step Hyp Ref Expression
1 usgr2pthlem.v V = Vtx G
2 usgr2pthlem.i I = iEdg G
3 1 2 usgr2pth G USGraph F Paths G P F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V z V x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
4 r19.42v y V x z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
5 rexdifpr y V x z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
6 4 5 bitr3i z x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
7 6 rexbii z V z x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z V y V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
8 rexcom z V y V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V z V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
9 df-3an y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
10 anass y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
11 anass z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
12 anass y x y z z x y x y z z x
13 ancom y x y z z x y z z x y x
14 necom y z z y
15 14 anbi2ci y z z x z x z y
16 15 anbi1i y z z x y x z x z y y x
17 12 13 16 3bitri y x y z z x z x z y y x
18 17 anbi1i y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
19 df-3an z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
20 11 18 19 3bitr4i y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
21 9 10 20 3bitr2i y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
22 21 rexbii z V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z V z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
23 rexdifpr z V x y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z V z x z y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
24 r19.42v z V x y y x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
25 22 23 24 3bitr2i z V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
26 25 rexbii y V z V y x y z z x P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V y x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
27 7 8 26 3bitri z V z x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V y x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
28 rexdifsn z V x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y z V z x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
29 rexdifsn y V x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V y x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
30 27 28 29 3bitr4i z V x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
31 30 a1i G USGraph x V z V x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y y V x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
32 31 rexbidva G USGraph x V z V x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y x V y V x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
33 32 3anbi3d G USGraph F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V z V x y V x z P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y
34 3 33 bitrd G USGraph F Paths G P F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = z P 2 = y I F 0 = x z I F 1 = z y