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 ) |