Metamath Proof Explorer

Theorem 1conngr

Description: A graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion 1conngr ⊢ G ∈ W ∧ Vtx ⁡ G = N → G ∈ ConnGraph

Proof

Step Hyp Ref Expression
1 snidg ⊢ N ∈ V → N ∈ N
2 1 adantr ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → N ∈ N
3 eleq2 ⊢ Vtx ⁡ G = N → N ∈ Vtx ⁡ G ↔ N ∈ N
4 3 ad2antll ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → N ∈ Vtx ⁡ G ↔ N ∈ N
5 2 4 mpbird ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → N ∈ Vtx ⁡ G
6 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
7 6 0pthonv ⊢ N ∈ Vtx ⁡ G → ∃ f ∃ p f N PathsOn ⁡ G N p
8 5 7 syl ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → ∃ f ∃ p f N PathsOn ⁡ G N p
9 oveq2 ⊢ n = N → N PathsOn ⁡ G n = N PathsOn ⁡ G N
10 9 breqd ⊢ n = N → f N PathsOn ⁡ G n p ↔ f N PathsOn ⁡ G N p
11 10 2exbidv ⊢ n = N → ∃ f ∃ p f N PathsOn ⁡ G n p ↔ ∃ f ∃ p f N PathsOn ⁡ G N p
12 11 ralsng ⊢ N ∈ V → ∀ n ∈ N ∃ f ∃ p f N PathsOn ⁡ G n p ↔ ∃ f ∃ p f N PathsOn ⁡ G N p
13 12 adantr ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → ∀ n ∈ N ∃ f ∃ p f N PathsOn ⁡ G n p ↔ ∃ f ∃ p f N PathsOn ⁡ G N p
14 8 13 mpbird ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → ∀ n ∈ N ∃ f ∃ p f N PathsOn ⁡ G n p
15 oveq1 ⊢ k = N → k PathsOn ⁡ G n = N PathsOn ⁡ G n
16 15 breqd ⊢ k = N → f k PathsOn ⁡ G n p ↔ f N PathsOn ⁡ G n p
17 16 2exbidv ⊢ k = N → ∃ f ∃ p f k PathsOn ⁡ G n p ↔ ∃ f ∃ p f N PathsOn ⁡ G n p
18 17 ralbidv ⊢ k = N → ∀ n ∈ N ∃ f ∃ p f k PathsOn ⁡ G n p ↔ ∀ n ∈ N ∃ f ∃ p f N PathsOn ⁡ G n p
19 18 ralsng ⊢ N ∈ V → ∀ k ∈ N ∀ n ∈ N ∃ f ∃ p f k PathsOn ⁡ G n p ↔ ∀ n ∈ N ∃ f ∃ p f N PathsOn ⁡ G n p
20 19 adantr ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → ∀ k ∈ N ∀ n ∈ N ∃ f ∃ p f k PathsOn ⁡ G n p ↔ ∀ n ∈ N ∃ f ∃ p f N PathsOn ⁡ G n p
21 14 20 mpbird ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → ∀ k ∈ N ∀ n ∈ N ∃ f ∃ p f k PathsOn ⁡ G n p
22 raleq ⊢ Vtx ⁡ G = N → ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p ↔ ∀ n ∈ N ∃ f ∃ p f k PathsOn ⁡ G n p
23 22 raleqbi1dv ⊢ Vtx ⁡ G = N → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p ↔ ∀ k ∈ N ∀ n ∈ N ∃ f ∃ p f k PathsOn ⁡ G n p
24 23 ad2antll ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p ↔ ∀ k ∈ N ∀ n ∈ N ∃ f ∃ p f k PathsOn ⁡ G n p
25 21 24 mpbird ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p
26 6 isconngr ⊢ G ∈ W → G ∈ ConnGraph ↔ ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p
27 26 ad2antrl ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → G ∈ ConnGraph ↔ ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p
28 25 27 mpbird ⊢ N ∈ V ∧ G ∈ W ∧ Vtx ⁡ G = N → G ∈ ConnGraph
29 28 ex ⊢ N ∈ V → G ∈ W ∧ Vtx ⁡ G = N → G ∈ ConnGraph
30 snprc ⊢ ¬ N ∈ V ↔ N = ∅
31 eqeq2 ⊢ N = ∅ → Vtx ⁡ G = N ↔ Vtx ⁡ G = ∅
32 31 anbi2d ⊢ N = ∅ → G ∈ W ∧ Vtx ⁡ G = N ↔ G ∈ W ∧ Vtx ⁡ G = ∅
33 0vconngr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ ConnGraph
34 32 33 biimtrdi ⊢ N = ∅ → G ∈ W ∧ Vtx ⁡ G = N → G ∈ ConnGraph
35 30 34 sylbi ⊢ ¬ N ∈ V → G ∈ W ∧ Vtx ⁡ G = N → G ∈ ConnGraph
36 29 35 pm2.61i ⊢ G ∈ W ∧ Vtx ⁡ G = N → G ∈ ConnGraph