Metamath Proof Explorer


Theorem isconngr1

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 isconngr1 G W G ConnGraph k V n V k f p f k PathsOn G n p

Proof

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