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 ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → 𝐺 ∈ ConnGraph )

Proof

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