Metamath Proof Explorer

Theorem isconngr1

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 isconngr1 ⊢ G ∈ W → G ∈ ConnGraph ↔ ∀ k ∈ V ∀ n ∈ V ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p

Proof

Step Hyp Ref Expression
1 isconngr.v ⊢ V = Vtx ⁡ G
2 dfconngr1 ⊢ ConnGraph = g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
3 2 eleq2i ⊢ G ∈ ConnGraph ↔ G ∈ g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
4 fvex ⊢ Vtx ⁡ g ∈ V
5 id ⊢ v = Vtx ⁡ g → v = Vtx ⁡ g
6 difeq1 ⊢ v = Vtx ⁡ g → v ∖ k = Vtx ⁡ g ∖ k
7 6 raleqdv ⊢ v = Vtx ⁡ g → ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
8 5 7 raleqbidv ⊢ v = Vtx ⁡ g → ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
9 4 8 sbcie ⊢ [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
10 9 abbii ⊢ g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p = g | ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
11 10 eleq2i ⊢ G ∈ g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ G ∈ g | ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p
12 fveq2 ⊢ h = G → Vtx ⁡ h = Vtx ⁡ G
13 12 1 eqtr4di ⊢ h = G → Vtx ⁡ h = V
14 13 difeq1d ⊢ h = G → Vtx ⁡ h ∖ k = V ∖ k
15 fveq2 ⊢ h = G → PathsOn ⁡ h = PathsOn ⁡ G
16 15 oveqd ⊢ h = G → k PathsOn ⁡ h n = k PathsOn ⁡ G n
17 16 breqd ⊢ h = G → f k PathsOn ⁡ h n p ↔ f k PathsOn ⁡ G n p
18 17 2exbidv ⊢ h = G → ∃ f ∃ p f k PathsOn ⁡ h n p ↔ ∃ f ∃ p f k PathsOn ⁡ G n p
19 14 18 raleqbidv ⊢ h = G → ∀ n ∈ Vtx ⁡ h ∖ k ∃ f ∃ p f k PathsOn ⁡ h n p ↔ ∀ n ∈ V ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p
20 13 19 raleqbidv ⊢ h = G → ∀ k ∈ Vtx ⁡ h ∀ n ∈ Vtx ⁡ h ∖ k ∃ f ∃ p f k PathsOn ⁡ h n p ↔ ∀ k ∈ V ∀ n ∈ V ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p
21 fveq2 ⊢ g = h → Vtx ⁡ g = Vtx ⁡ h
22 21 difeq1d ⊢ g = h → Vtx ⁡ g ∖ k = Vtx ⁡ h ∖ k
23 fveq2 ⊢ g = h → PathsOn ⁡ g = PathsOn ⁡ h
24 23 oveqd ⊢ g = h → k PathsOn ⁡ g n = k PathsOn ⁡ h n
25 24 breqd ⊢ g = h → f k PathsOn ⁡ g n p ↔ f k PathsOn ⁡ h n p
26 25 2exbidv ⊢ g = h → ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∃ f ∃ p f k PathsOn ⁡ h n p
27 22 26 raleqbidv ⊢ g = h → ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ n ∈ Vtx ⁡ h ∖ k ∃ f ∃ p f k PathsOn ⁡ h n p
28 21 27 raleqbidv ⊢ g = h → ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ Vtx ⁡ h ∀ n ∈ Vtx ⁡ h ∖ k ∃ f ∃ p f k PathsOn ⁡ h n p
29 28 cbvabv ⊢ g | ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p = h | ∀ k ∈ Vtx ⁡ h ∀ n ∈ Vtx ⁡ h ∖ k ∃ f ∃ p f k PathsOn ⁡ h n p
30 20 29 elab2g ⊢ G ∈ W → G ∈ g | ∀ k ∈ Vtx ⁡ g ∀ n ∈ Vtx ⁡ g ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ V ∀ n ∈ V ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p
31 11 30 syl5bb ⊢ G ∈ W → G ∈ g | [˙ Vtx ⁡ g / v]˙ ∀ k ∈ v ∀ n ∈ v ∖ k ∃ f ∃ p f k PathsOn ⁡ g n p ↔ ∀ k ∈ V ∀ n ∈ V ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p
32 3 31 syl5bb ⊢ G ∈ W → G ∈ ConnGraph ↔ ∀ k ∈ V ∀ n ∈ V ∖ k ∃ f ∃ p f k PathsOn ⁡ G n p