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 ∃ p f k PathsOn ⁡ G n p

Proof

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