Metamath Proof Explorer


Theorem isconngr

Description: The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Hypothesis isconngr.v V = Vtx G
Assertion isconngr G W G ConnGraph k V n V f p f k PathsOn G n p

Proof

Step Hyp Ref Expression
1 isconngr.v V = Vtx G
2 df-conngr ConnGraph = g | [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p
3 2 eleq2i G ConnGraph G g | [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p
4 fvex Vtx g V
5 raleq v = Vtx g n v f p f k PathsOn g n p n Vtx g f p f k PathsOn g n p
6 5 raleqbi1dv v = Vtx g k v n v f p f k PathsOn g n p k Vtx g n Vtx g f p f k PathsOn g n p
7 4 6 sbcie [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p k Vtx g n Vtx g f p f k PathsOn g n p
8 7 abbii g | [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p = g | k Vtx g n Vtx g f p f k PathsOn g n p
9 8 eleq2i G g | [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p G g | k Vtx g n Vtx g f p f k PathsOn g n p
10 fveq2 h = G Vtx h = Vtx G
11 10 1 eqtr4di h = G Vtx h = V
12 fveq2 h = G PathsOn h = PathsOn G
13 12 oveqd h = G k PathsOn h n = k PathsOn G n
14 13 breqd h = G f k PathsOn h n p f k PathsOn G n p
15 14 2exbidv h = G f p f k PathsOn h n p f p f k PathsOn G n p
16 11 15 raleqbidv h = G n Vtx h f p f k PathsOn h n p n V f p f k PathsOn G n p
17 11 16 raleqbidv h = G k Vtx h n Vtx h f p f k PathsOn h n p k V n V f p f k PathsOn G n p
18 fveq2 g = h Vtx g = Vtx h
19 fveq2 g = h PathsOn g = PathsOn h
20 19 oveqd g = h k PathsOn g n = k PathsOn h n
21 20 breqd g = h f k PathsOn g n p f k PathsOn h n p
22 21 2exbidv g = h f p f k PathsOn g n p f p f k PathsOn h n p
23 18 22 raleqbidv g = h n Vtx g f p f k PathsOn g n p n Vtx h f p f k PathsOn h n p
24 18 23 raleqbidv g = h k Vtx g n Vtx g f p f k PathsOn g n p k Vtx h n Vtx h f p f k PathsOn h n p
25 24 cbvabv g | k Vtx g n Vtx g f p f k PathsOn g n p = h | k Vtx h n Vtx h f p f k PathsOn h n p
26 17 25 elab2g G W G g | k Vtx g n Vtx g f p f k PathsOn g n p k V n V f p f k PathsOn G n p
27 9 26 syl5bb G W G g | [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p k V n V f p f k PathsOn G n p
28 3 27 syl5bb G W G ConnGraph k V n V f p f k PathsOn G n p