MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isconngr Structured version   Visualization version   GIF version

Theorem isconngr 29442
Description: The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.)
Hypothesis
Ref Expression
isconngr.v 𝑉 = (Vtxβ€˜πΊ)
Assertion
Ref Expression
isconngr (𝐺 ∈ π‘Š β†’ (𝐺 ∈ ConnGraph ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
Distinct variable groups:   𝑓,π‘˜,𝑛,𝑝,𝐺   π‘˜,𝑉,𝑛
Allowed substitution hints:   𝑉(𝑓,𝑝)   π‘Š(𝑓,π‘˜,𝑛,𝑝)

Proof of Theorem isconngr
Dummy variables 𝑔 β„Ž 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-conngr 29440 . . 3 ConnGraph = {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝}
21eleq2i 2826 . 2 (𝐺 ∈ ConnGraph ↔ 𝐺 ∈ {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝})
3 fvex 6905 . . . . . 6 (Vtxβ€˜π‘”) ∈ V
4 raleq 3323 . . . . . . 7 (𝑣 = (Vtxβ€˜π‘”) β†’ (βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝))
54raleqbi1dv 3334 . . . . . 6 (𝑣 = (Vtxβ€˜π‘”) β†’ (βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝))
63, 5sbcie 3821 . . . . 5 ([(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝)
76abbii 2803 . . . 4 {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} = {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝}
87eleq2i 2826 . . 3 (𝐺 ∈ {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} ↔ 𝐺 ∈ {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝})
9 fveq2 6892 . . . . . 6 (β„Ž = 𝐺 β†’ (Vtxβ€˜β„Ž) = (Vtxβ€˜πΊ))
10 isconngr.v . . . . . 6 𝑉 = (Vtxβ€˜πΊ)
119, 10eqtr4di 2791 . . . . 5 (β„Ž = 𝐺 β†’ (Vtxβ€˜β„Ž) = 𝑉)
12 fveq2 6892 . . . . . . . . 9 (β„Ž = 𝐺 β†’ (PathsOnβ€˜β„Ž) = (PathsOnβ€˜πΊ))
1312oveqd 7426 . . . . . . . 8 (β„Ž = 𝐺 β†’ (π‘˜(PathsOnβ€˜β„Ž)𝑛) = (π‘˜(PathsOnβ€˜πΊ)𝑛))
1413breqd 5160 . . . . . . 7 (β„Ž = 𝐺 β†’ (𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
15142exbidv 1928 . . . . . 6 (β„Ž = 𝐺 β†’ (βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
1611, 15raleqbidv 3343 . . . . 5 (β„Ž = 𝐺 β†’ (βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
1711, 16raleqbidv 3343 . . . 4 (β„Ž = 𝐺 β†’ (βˆ€π‘˜ ∈ (Vtxβ€˜β„Ž)βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
18 fveq2 6892 . . . . . 6 (𝑔 = β„Ž β†’ (Vtxβ€˜π‘”) = (Vtxβ€˜β„Ž))
19 fveq2 6892 . . . . . . . . . 10 (𝑔 = β„Ž β†’ (PathsOnβ€˜π‘”) = (PathsOnβ€˜β„Ž))
2019oveqd 7426 . . . . . . . . 9 (𝑔 = β„Ž β†’ (π‘˜(PathsOnβ€˜π‘”)𝑛) = (π‘˜(PathsOnβ€˜β„Ž)𝑛))
2120breqd 5160 . . . . . . . 8 (𝑔 = β„Ž β†’ (𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
22212exbidv 1928 . . . . . . 7 (𝑔 = β„Ž β†’ (βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
2318, 22raleqbidv 3343 . . . . . 6 (𝑔 = β„Ž β†’ (βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
2418, 23raleqbidv 3343 . . . . 5 (𝑔 = β„Ž β†’ (βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ (Vtxβ€˜β„Ž)βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
2524cbvabv 2806 . . . 4 {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} = {β„Ž ∣ βˆ€π‘˜ ∈ (Vtxβ€˜β„Ž)βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝}
2617, 25elab2g 3671 . . 3 (𝐺 ∈ π‘Š β†’ (𝐺 ∈ {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
278, 26bitrid 283 . 2 (𝐺 ∈ π‘Š β†’ (𝐺 ∈ {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
282, 27bitrid 283 1 (𝐺 ∈ π‘Š β†’ (𝐺 ∈ ConnGraph ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  [wsbc 3778   class class class wbr 5149  β€˜cfv 6544  (class class class)co 7409  Vtxcvtx 28256  PathsOncpthson 28971  ConnGraphcconngr 29439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-conngr 29440
This theorem is referenced by:  0conngr  29445  0vconngr  29446  1conngr  29447  conngrv2edg  29448
  Copyright terms: Public domain W3C validator