# 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

### Proof

Step Hyp Ref Expression
1 df-conngr
2 eqid ${⊢}\mathrm{Vtx}\left({g}\right)=\mathrm{Vtx}\left({g}\right)$
3 2 0pthonv ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){k}\right){p}$
4 oveq2 ${⊢}{n}={k}\to {k}\mathrm{PathsOn}\left({g}\right){n}={k}\mathrm{PathsOn}\left({g}\right){k}$
5 4 breqd ${⊢}{n}={k}\to \left({f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔{f}\left({k}\mathrm{PathsOn}\left({g}\right){k}\right){p}\right)$
6 5 2exbidv ${⊢}{n}={k}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){k}\right){p}\right)$
7 6 ralsng ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \left(\forall {n}\in \left\{{k}\right\}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){k}\right){p}\right)$
8 3 7 mpbird ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \forall {n}\in \left\{{k}\right\}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}$
9 difsnid ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\cup \left\{{k}\right\}=\mathrm{Vtx}\left({g}\right)$
10 9 eqcomd ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \mathrm{Vtx}\left({g}\right)=\left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\cup \left\{{k}\right\}$
11 10 raleqdv ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \left(\forall {n}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {n}\in \left(\left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\cup \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)$
12 ralunb ${⊢}\forall {n}\in \left(\left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\cup \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\left(\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\wedge \forall {n}\in \left\{{k}\right\}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)$
13 11 12 syl6bb ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \left(\forall {n}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\left(\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\wedge \forall {n}\in \left\{{k}\right\}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)\right)$
14 8 13 mpbiran2d ${⊢}{k}\in \mathrm{Vtx}\left({g}\right)\to \left(\forall {n}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)$
15 14 ralbiia ${⊢}\forall {k}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {k}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}$
16 fvex ${⊢}\mathrm{Vtx}\left({g}\right)\in \mathrm{V}$
17 raleq ${⊢}{v}=\mathrm{Vtx}\left({g}\right)\to \left(\forall {n}\in {v}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {n}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)$
18 17 raleqbi1dv ${⊢}{v}=\mathrm{Vtx}\left({g}\right)\to \left(\forall {k}\in {v}\phantom{\rule{.4em}{0ex}}\forall {n}\in {v}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {k}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)$
19 difeq1 ${⊢}{v}=\mathrm{Vtx}\left({g}\right)\to {v}\setminus \left\{{k}\right\}=\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}$
20 19 raleqdv ${⊢}{v}=\mathrm{Vtx}\left({g}\right)\to \left(\forall {n}\in \left({v}\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)$
21 20 raleqbi1dv ${⊢}{v}=\mathrm{Vtx}\left({g}\right)\to \left(\forall {k}\in {v}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left({v}\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {k}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)$
22 18 21 bibi12d ${⊢}{v}=\mathrm{Vtx}\left({g}\right)\to \left(\left(\forall {k}\in {v}\phantom{\rule{.4em}{0ex}}\forall {n}\in {v}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {k}\in {v}\phantom{\rule{.4em}{0ex}}\forall {n}\in \left({v}\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)↔\left(\forall {k}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}↔\forall {k}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left(\mathrm{Vtx}\left({g}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {p}\phantom{\rule{.4em}{0ex}}{f}\left({k}\mathrm{PathsOn}\left({g}\right){n}\right){p}\right)\right)$
23 16 22 sbcie
24 15 23 mpbir
25 sbcbi1
26 24 25 ax-mp
27 26 abbii
28 1 27 eqtri