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 syl6bi ( { 𝑁 } = ∅ → ( ( 𝐺𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → 𝐺 ∈ ConnGraph ) )
35 30 34 sylbi ( ¬ 𝑁 ∈ V → ( ( 𝐺𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → 𝐺 ∈ ConnGraph ) )
36 29 35 pm2.61i ( ( 𝐺𝑊 ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → 𝐺 ∈ ConnGraph )