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

Theorem isconngr 29709
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 29707 . . 3 ConnGraph = {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝}
21eleq2i 2823 . 2 (𝐺 ∈ ConnGraph ↔ 𝐺 ∈ {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝})
3 fvex 6903 . . . . . 6 (Vtxβ€˜π‘”) ∈ V
4 raleq 3320 . . . . . . 7 (𝑣 = (Vtxβ€˜π‘”) β†’ (βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝))
54raleqbi1dv 3331 . . . . . 6 (𝑣 = (Vtxβ€˜π‘”) β†’ (βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝))
63, 5sbcie 3819 . . . . 5 ([(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝)
76abbii 2800 . . . 4 {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} = {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝}
87eleq2i 2823 . . 3 (𝐺 ∈ {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} ↔ 𝐺 ∈ {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝})
9 fveq2 6890 . . . . . 6 (β„Ž = 𝐺 β†’ (Vtxβ€˜β„Ž) = (Vtxβ€˜πΊ))
10 isconngr.v . . . . . 6 𝑉 = (Vtxβ€˜πΊ)
119, 10eqtr4di 2788 . . . . 5 (β„Ž = 𝐺 β†’ (Vtxβ€˜β„Ž) = 𝑉)
12 fveq2 6890 . . . . . . . . 9 (β„Ž = 𝐺 β†’ (PathsOnβ€˜β„Ž) = (PathsOnβ€˜πΊ))
1312oveqd 7428 . . . . . . . 8 (β„Ž = 𝐺 β†’ (π‘˜(PathsOnβ€˜β„Ž)𝑛) = (π‘˜(PathsOnβ€˜πΊ)𝑛))
1413breqd 5158 . . . . . . 7 (β„Ž = 𝐺 β†’ (𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
15142exbidv 1925 . . . . . 6 (β„Ž = 𝐺 β†’ (βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
1611, 15raleqbidv 3340 . . . . 5 (β„Ž = 𝐺 β†’ (βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
1711, 16raleqbidv 3340 . . . 4 (β„Ž = 𝐺 β†’ (βˆ€π‘˜ ∈ (Vtxβ€˜β„Ž)βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
18 fveq2 6890 . . . . . 6 (𝑔 = β„Ž β†’ (Vtxβ€˜π‘”) = (Vtxβ€˜β„Ž))
19 fveq2 6890 . . . . . . . . . 10 (𝑔 = β„Ž β†’ (PathsOnβ€˜π‘”) = (PathsOnβ€˜β„Ž))
2019oveqd 7428 . . . . . . . . 9 (𝑔 = β„Ž β†’ (π‘˜(PathsOnβ€˜π‘”)𝑛) = (π‘˜(PathsOnβ€˜β„Ž)𝑛))
2120breqd 5158 . . . . . . . 8 (𝑔 = β„Ž β†’ (𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
22212exbidv 1925 . . . . . . 7 (𝑔 = β„Ž β†’ (βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
2318, 22raleqbidv 3340 . . . . . 6 (𝑔 = β„Ž β†’ (βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
2418, 23raleqbidv 3340 . . . . 5 (𝑔 = β„Ž β†’ (βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝 ↔ βˆ€π‘˜ ∈ (Vtxβ€˜β„Ž)βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝))
2524cbvabv 2803 . . . 4 {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} = {β„Ž ∣ βˆ€π‘˜ ∈ (Vtxβ€˜β„Ž)βˆ€π‘› ∈ (Vtxβ€˜β„Ž)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜β„Ž)𝑛)𝑝}
2617, 25elab2g 3669 . . 3 (𝐺 ∈ π‘Š β†’ (𝐺 ∈ {𝑔 ∣ βˆ€π‘˜ ∈ (Vtxβ€˜π‘”)βˆ€π‘› ∈ (Vtxβ€˜π‘”)βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
278, 26bitrid 282 . 2 (𝐺 ∈ π‘Š β†’ (𝐺 ∈ {𝑔 ∣ [(Vtxβ€˜π‘”) / 𝑣]βˆ€π‘˜ ∈ 𝑣 βˆ€π‘› ∈ 𝑣 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜π‘”)𝑛)𝑝} ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
282, 27bitrid 282 1 (𝐺 ∈ π‘Š β†’ (𝐺 ∈ ConnGraph ↔ βˆ€π‘˜ ∈ 𝑉 βˆ€π‘› ∈ 𝑉 βˆƒπ‘“βˆƒπ‘ 𝑓(π‘˜(PathsOnβ€˜πΊ)𝑛)𝑝))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104  {cab 2707  βˆ€wral 3059  [wsbc 3776   class class class wbr 5147  β€˜cfv 6542  (class class class)co 7411  Vtxcvtx 28523  PathsOncpthson 29238  ConnGraphcconngr 29706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414  df-conngr 29707
This theorem is referenced by:  0conngr  29712  0vconngr  29713  1conngr  29714  conngrv2edg  29715
  Copyright terms: Public domain W3C validator