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=VtxG
Assertion isconngr1 GWGConnGraphkVnVkfpfkPathsOnGnp

Proof

Step Hyp Ref Expression
1 isconngr.v V=VtxG
2 dfconngr1 ConnGraph=g|[˙Vtxg/v]˙kvnvkfpfkPathsOngnp
3 2 eleq2i GConnGraphGg|[˙Vtxg/v]˙kvnvkfpfkPathsOngnp
4 fvex VtxgV
5 id v=Vtxgv=Vtxg
6 difeq1 v=Vtxgvk=Vtxgk
7 6 raleqdv v=VtxgnvkfpfkPathsOngnpnVtxgkfpfkPathsOngnp
8 5 7 raleqbidv v=VtxgkvnvkfpfkPathsOngnpkVtxgnVtxgkfpfkPathsOngnp
9 4 8 sbcie [˙Vtxg/v]˙kvnvkfpfkPathsOngnpkVtxgnVtxgkfpfkPathsOngnp
10 9 abbii g|[˙Vtxg/v]˙kvnvkfpfkPathsOngnp=g|kVtxgnVtxgkfpfkPathsOngnp
11 10 eleq2i Gg|[˙Vtxg/v]˙kvnvkfpfkPathsOngnpGg|kVtxgnVtxgkfpfkPathsOngnp
12 fveq2 h=GVtxh=VtxG
13 12 1 eqtr4di h=GVtxh=V
14 13 difeq1d h=GVtxhk=Vk
15 fveq2 h=GPathsOnh=PathsOnG
16 15 oveqd h=GkPathsOnhn=kPathsOnGn
17 16 breqd h=GfkPathsOnhnpfkPathsOnGnp
18 17 2exbidv h=GfpfkPathsOnhnpfpfkPathsOnGnp
19 14 18 raleqbidv h=GnVtxhkfpfkPathsOnhnpnVkfpfkPathsOnGnp
20 13 19 raleqbidv h=GkVtxhnVtxhkfpfkPathsOnhnpkVnVkfpfkPathsOnGnp
21 fveq2 g=hVtxg=Vtxh
22 21 difeq1d g=hVtxgk=Vtxhk
23 fveq2 g=hPathsOng=PathsOnh
24 23 oveqd g=hkPathsOngn=kPathsOnhn
25 24 breqd g=hfkPathsOngnpfkPathsOnhnp
26 25 2exbidv g=hfpfkPathsOngnpfpfkPathsOnhnp
27 22 26 raleqbidv g=hnVtxgkfpfkPathsOngnpnVtxhkfpfkPathsOnhnp
28 21 27 raleqbidv g=hkVtxgnVtxgkfpfkPathsOngnpkVtxhnVtxhkfpfkPathsOnhnp
29 28 cbvabv g|kVtxgnVtxgkfpfkPathsOngnp=h|kVtxhnVtxhkfpfkPathsOnhnp
30 20 29 elab2g GWGg|kVtxgnVtxgkfpfkPathsOngnpkVnVkfpfkPathsOnGnp
31 11 30 syl5bb GWGg|[˙Vtxg/v]˙kvnvkfpfkPathsOngnpkVnVkfpfkPathsOnGnp
32 3 31 syl5bb GWGConnGraphkVnVkfpfkPathsOnGnp