Metamath Proof Explorer


Theorem dfconngr1

Description: Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion dfconngr1 ConnGraph = g | [˙ Vtx g / v]˙ k v n v k f p f k PathsOn g n p

Proof

Step Hyp Ref Expression
1 df-conngr ConnGraph = g | [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p
2 eqid Vtx g = Vtx g
3 2 0pthonv k Vtx g f p f k PathsOn g k p
4 oveq2 n = k k PathsOn g n = k PathsOn g k
5 4 breqd n = k f k PathsOn g n p f k PathsOn g k p
6 5 2exbidv n = k f p f k PathsOn g n p f p f k PathsOn g k p
7 6 ralsng k Vtx g n k f p f k PathsOn g n p f p f k PathsOn g k p
8 3 7 mpbird k Vtx g n k f p f k PathsOn g n p
9 difsnid k Vtx g Vtx g k k = Vtx g
10 9 eqcomd k Vtx g Vtx g = Vtx g k k
11 10 raleqdv k Vtx g n Vtx g f p f k PathsOn g n p n Vtx g k k f p f k PathsOn g n p
12 ralunb n Vtx g k k f p f k PathsOn g n p n Vtx g k f p f k PathsOn g n p n k f p f k PathsOn g n p
13 11 12 bitrdi k Vtx g n Vtx g f p f k PathsOn g n p n Vtx g k f p f k PathsOn g n p n k f p f k PathsOn g n p
14 8 13 mpbiran2d k Vtx g n Vtx g f p f k PathsOn g n p n Vtx g k f p f k PathsOn g n p
15 14 ralbiia k Vtx g n Vtx g f p f k PathsOn g n p k Vtx g n Vtx g k f p f k PathsOn g n p
16 fvex Vtx g V
17 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
18 17 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
19 difeq1 v = Vtx g v k = Vtx g k
20 19 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
21 20 raleqbi1dv 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
22 18 21 bibi12d v = Vtx g k v n v f p f k PathsOn g n p k v n v k f p f k PathsOn g n p k Vtx g n Vtx g f p f k PathsOn g n p k Vtx g n Vtx g k f p f k PathsOn g n p
23 16 22 sbcie [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p k v n v k f p f k PathsOn g n p k Vtx g n Vtx g f p f k PathsOn g n p k Vtx g n Vtx g k f p f k PathsOn g n p
24 15 23 mpbir [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p k v n v k f p f k PathsOn g n p
25 sbcbi1 [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p k v n v k f p f k PathsOn g n p [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p [˙ Vtx g / v]˙ k v n v k f p f k PathsOn g n p
26 24 25 ax-mp [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p [˙ Vtx g / v]˙ k v n v k f p f k PathsOn g n p
27 26 abbii g | [˙ Vtx g / v]˙ k v n v f p f k PathsOn g n p = g | [˙ Vtx g / v]˙ k v n v k f p f k PathsOn g n p
28 1 27 eqtri ConnGraph = g | [˙ Vtx g / v]˙ k v n v k f p f k PathsOn g n p