Theorem isconngr 30392

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.

Step	Hyp	Ref	Expression
1		df-conngr 30390	. . 3 ⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝}
2	1	eleq2i 2855	. 2 ⊢ (𝐺 ∈ ConnGraph ↔ 𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝})
3		fvex 6881	. . . . . 6 ⊢ (Vtx‘𝑔) ∈ V
4		raleq 3318	. . . . . . 7 ⊢ (𝑣 = (Vtx‘𝑔) → (∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 ↔ ∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝))
5	4	raleqbi1dv 3331	. . . . . 6 ⊢ (𝑣 = (Vtx‘𝑔) → (∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 ↔ ∀𝑘 ∈ (Vtx‘𝑔)∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝))
6	3, 5	sbcie 3786	. . . . 5 ⊢ ([(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 ↔ ∀𝑘 ∈ (Vtx‘𝑔)∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝)
7	6	abbii 2830	. . . 4 ⊢ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} = {𝑔 ∣ ∀𝑘 ∈ (Vtx‘𝑔)∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝}
8	7	eleq2i 2855	. . 3 ⊢ (𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} ↔ 𝐺 ∈ {𝑔 ∣ ∀𝑘 ∈ (Vtx‘𝑔)∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝})
9		fveq2 6868	. . . . . 6 ⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = (Vtx‘𝐺))
10		isconngr.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
11	9, 10	eqtr4di 2816	. . . . 5 ⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = 𝑉)
12		fveq2 6868	. . . . . . . . 9 ⊢ (ℎ = 𝐺 → (PathsOn‘ℎ) = (PathsOn‘𝐺))
13	12	oveqd 7414	. . . . . . . 8 ⊢ (ℎ = 𝐺 → (𝑘(PathsOn‘ℎ)𝑛) = (𝑘(PathsOn‘𝐺)𝑛))
14	13	breqd 5112	. . . . . . 7 ⊢ (ℎ = 𝐺 → (𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝 ↔ 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝))
15	14	2exbidv 1945	. . . . . 6 ⊢ (ℎ = 𝐺 → (∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝 ↔ ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝))
16	11, 15	raleqbidv 3337	. . . . 5 ⊢ (ℎ = 𝐺 → (∀𝑛 ∈ (Vtx‘ℎ)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝 ↔ ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝))
17	11, 16	raleqbidv 3337	. . . 4 ⊢ (ℎ = 𝐺 → (∀𝑘 ∈ (Vtx‘ℎ)∀𝑛 ∈ (Vtx‘ℎ)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝 ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝))
18		fveq2 6868	. . . . . 6 ⊢ (𝑔 = ℎ → (Vtx‘𝑔) = (Vtx‘ℎ))
19		fveq2 6868	. . . . . . . . . 10 ⊢ (𝑔 = ℎ → (PathsOn‘𝑔) = (PathsOn‘ℎ))
20	19	oveqd 7414	. . . . . . . . 9 ⊢ (𝑔 = ℎ → (𝑘(PathsOn‘𝑔)𝑛) = (𝑘(PathsOn‘ℎ)𝑛))
21	20	breqd 5112	. . . . . . . 8 ⊢ (𝑔 = ℎ → (𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 ↔ 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝))
22	21	2exbidv 1945	. . . . . . 7 ⊢ (𝑔 = ℎ → (∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 ↔ ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝))
23	18, 22	raleqbidv 3337	. . . . . 6 ⊢ (𝑔 = ℎ → (∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 ↔ ∀𝑛 ∈ (Vtx‘ℎ)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝))
24	18, 23	raleqbidv 3337	. . . . 5 ⊢ (𝑔 = ℎ → (∀𝑘 ∈ (Vtx‘𝑔)∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝 ↔ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑛 ∈ (Vtx‘ℎ)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝))
25	24	cbvabv 2833	. . . 4 ⊢ {𝑔 ∣ ∀𝑘 ∈ (Vtx‘𝑔)∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} = {ℎ ∣ ∀𝑘 ∈ (Vtx‘ℎ)∀𝑛 ∈ (Vtx‘ℎ)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘ℎ)𝑛)𝑝}
26	17, 25	elab2g 3640	. . 3 ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ {𝑔 ∣ ∀𝑘 ∈ (Vtx‘𝑔)∀𝑛 ∈ (Vtx‘𝑔)∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝))
27	8, 26	bitrid 285	. 2 ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝))
28	2, 27	bitrid 285	1 ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ConnGraph ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561  ∃wex 1800   ∈ wcel 2143  {cab 2741  ∀wral 3077  [wsbc 3745   class class class wbr 5101  ‘cfv 6522  (class class class)co 7397  Vtxcvtx 29198  PathsOncpthson 29913  ConnGraphcconngr 30389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5257

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6478  df-fv 6530  df-ov 7400  df-conngr 30390

This theorem is referenced by:  0conngr  30395  0vconngr  30396  1conngr  30397  conngrv2edg  30398