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∃pfkPathsOn⁡Gnp

Proof

Step Hyp Ref Expression
1 isconngr.v ⊢V=Vtx⁡G
2 df-conngr ⊢ConnGraph=g|[˙Vtx⁡g/v]˙∀k∈v∀n∈v∃f∃pfkPathsOn⁡gnp
3 2 eleq2i ⊢G∈ConnGraph↔G∈g|[˙Vtx⁡g/v]˙∀k∈v∀n∈v∃f∃pfkPathsOn⁡gnp
4 fvex ⊢Vtx⁡g∈V
5 raleq ⊢v=Vtx⁡g→∀n∈v∃f∃pfkPathsOn⁡gnp↔∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp
6 5 raleqbi1dv ⊢v=Vtx⁡g→∀k∈v∀n∈v∃f∃pfkPathsOn⁡gnp↔∀k∈Vtx⁡g∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp
7 4 6 sbcie ⊢[˙Vtx⁡g/v]˙∀k∈v∀n∈v∃f∃pfkPathsOn⁡gnp↔∀k∈Vtx⁡g∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp
8 7 abbii ⊢g|[˙Vtx⁡g/v]˙∀k∈v∀n∈v∃f∃pfkPathsOn⁡gnp=g|∀k∈Vtx⁡g∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp
9 8 eleq2i ⊢G∈g|[˙Vtx⁡g/v]˙∀k∈v∀n∈v∃f∃pfkPathsOn⁡gnp↔G∈g|∀k∈Vtx⁡g∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp
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→kPathsOn⁡hn=kPathsOn⁡Gn
14 13 breqd ⊢h=G→fkPathsOn⁡hnp↔fkPathsOn⁡Gnp
15 14 2exbidv ⊢h=G→∃f∃pfkPathsOn⁡hnp↔∃f∃pfkPathsOn⁡Gnp
16 11 15 raleqbidv ⊢h=G→∀n∈Vtx⁡h∃f∃pfkPathsOn⁡hnp↔∀n∈V∃f∃pfkPathsOn⁡Gnp
17 11 16 raleqbidv ⊢h=G→∀k∈Vtx⁡h∀n∈Vtx⁡h∃f∃pfkPathsOn⁡hnp↔∀k∈V∀n∈V∃f∃pfkPathsOn⁡Gnp
18 fveq2 ⊢g=h→Vtx⁡g=Vtx⁡h
19 fveq2 ⊢g=h→PathsOn⁡g=PathsOn⁡h
20 19 oveqd ⊢g=h→kPathsOn⁡gn=kPathsOn⁡hn
21 20 breqd ⊢g=h→fkPathsOn⁡gnp↔fkPathsOn⁡hnp
22 21 2exbidv ⊢g=h→∃f∃pfkPathsOn⁡gnp↔∃f∃pfkPathsOn⁡hnp
23 18 22 raleqbidv ⊢g=h→∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp↔∀n∈Vtx⁡h∃f∃pfkPathsOn⁡hnp
24 18 23 raleqbidv ⊢g=h→∀k∈Vtx⁡g∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp↔∀k∈Vtx⁡h∀n∈Vtx⁡h∃f∃pfkPathsOn⁡hnp
25 24 cbvabv ⊢g|∀k∈Vtx⁡g∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp=h|∀k∈Vtx⁡h∀n∈Vtx⁡h∃f∃pfkPathsOn⁡hnp
26 17 25 elab2g ⊢G∈W→G∈g|∀k∈Vtx⁡g∀n∈Vtx⁡g∃f∃pfkPathsOn⁡gnp↔∀k∈V∀n∈V∃f∃pfkPathsOn⁡Gnp
27 9 26 bitrid ⊢G∈W→G∈g|[˙Vtx⁡g/v]˙∀k∈v∀n∈v∃f∃pfkPathsOn⁡gnp↔∀k∈V∀n∈V∃f∃pfkPathsOn⁡Gnp
28 3 27 bitrid ⊢G∈W→G∈ConnGraph↔∀k∈V∀n∈V∃f∃pfkPathsOn⁡Gnp