Step |
Hyp |
Ref |
Expression |
1 |
|
df-conngr |
⊢ ConnGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } |
2 |
|
eqid |
⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 ) |
3 |
2
|
0pthonv |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑘 ) 𝑝 ) |
4 |
|
oveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) = ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑘 ) ) |
5 |
4
|
breqd |
⊢ ( 𝑛 = 𝑘 → ( 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑘 ) 𝑝 ) ) |
6 |
5
|
2exbidv |
⊢ ( 𝑛 = 𝑘 → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑘 ) 𝑝 ) ) |
7 |
6
|
ralsng |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ( ∀ 𝑛 ∈ { 𝑘 } ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑘 ) 𝑝 ) ) |
8 |
3 7
|
mpbird |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ∀ 𝑛 ∈ { 𝑘 } ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) |
9 |
|
difsnid |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ( ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∪ { 𝑘 } ) = ( Vtx ‘ 𝑔 ) ) |
10 |
9
|
eqcomd |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ( Vtx ‘ 𝑔 ) = ( ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∪ { 𝑘 } ) ) |
11 |
10
|
raleqdv |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ( ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑛 ∈ ( ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∪ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
12 |
|
ralunb |
⊢ ( ∀ 𝑛 ∈ ( ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∪ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ∧ ∀ 𝑛 ∈ { 𝑘 } ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
13 |
11 12
|
syl6bb |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ( ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ∧ ∀ 𝑛 ∈ { 𝑘 } ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) ) |
14 |
8 13
|
mpbiran2d |
⊢ ( 𝑘 ∈ ( Vtx ‘ 𝑔 ) → ( ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
15 |
14
|
ralbiia |
⊢ ( ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) |
16 |
|
fvex |
⊢ ( Vtx ‘ 𝑔 ) ∈ V |
17 |
|
raleq |
⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
18 |
17
|
raleqbi1dv |
⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
19 |
|
difeq1 |
⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( 𝑣 ∖ { 𝑘 } ) = ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ) |
20 |
19
|
raleqdv |
⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
21 |
20
|
raleqbi1dv |
⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
22 |
18 21
|
bibi12d |
⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ↔ ( ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) ) |
23 |
16 22
|
sbcie |
⊢ ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ↔ ( ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝑔 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
24 |
15 23
|
mpbir |
⊢ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) |
25 |
|
sbcbi1 |
⊢ ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) → ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) ) |
26 |
24 25
|
ax-mp |
⊢ ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) |
27 |
26
|
abbii |
⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } |
28 |
1 27
|
eqtri |
⊢ ConnGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } |