Metamath Proof Explorer

Theorem isconngr

Description: The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Hypothesis isconngr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion isconngr ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )

Proof

Step Hyp Ref Expression
1 isconngr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 df-conngr ⊢ ConnGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 }
3 2 eleq2i ⊢ ( 𝐺 ∈ ConnGraph ↔ 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } )
4 fvex ⊢ ( Vtx ‘ 𝑔 ) ∈ V
5 raleq ⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) )
6 5 raleqbi1dv ⊢ ( 𝑣 = ( Vtx ‘ 𝑔 ) → ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ) )
7 4 6 sbcie ⊢ ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 )
8 7 abbii ⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } = { 𝑔 ∣ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 }
9 8 eleq2i ⊢ ( 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } ↔ 𝐺 ∈ { 𝑔 ∣ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } )
10 fveq2 ⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐺 ) )
11 10 1 eqtr4di ⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = 𝑉 )
12 fveq2 ⊢ ( ℎ = 𝐺 → ( PathsOn ‘ ℎ ) = ( PathsOn ‘ 𝐺 ) )
13 12 oveqd ⊢ ( ℎ = 𝐺 → ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) = ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) )
14 13 breqd ⊢ ( ℎ = 𝐺 → ( 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ↔ 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
15 14 2exbidv ⊢ ( ℎ = 𝐺 → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
16 11 15 raleqbidv ⊢ ( ℎ = 𝐺 → ( ∀ 𝑛 ∈ ( Vtx ‘ ℎ ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ↔ ∀ 𝑛 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
17 11 16 raleqbidv ⊢ ( ℎ = 𝐺 → ( ∀ 𝑘 ∈ ( Vtx ‘ ℎ ) ∀ 𝑛 ∈ ( Vtx ‘ ℎ ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
18 fveq2 ⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ ℎ ) )
19 fveq2 ⊢ ( 𝑔 = ℎ → ( PathsOn ‘ 𝑔 ) = ( PathsOn ‘ ℎ ) )
20 19 oveqd ⊢ ( 𝑔 = ℎ → ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) = ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) )
21 20 breqd ⊢ ( 𝑔 = ℎ → ( 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ) )
22 21 2exbidv ⊢ ( 𝑔 = ℎ → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ) )
23 18 22 raleqbidv ⊢ ( 𝑔 = ℎ → ( ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑛 ∈ ( Vtx ‘ ℎ ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ) )
24 18 23 raleqbidv ⊢ ( 𝑔 = ℎ → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 ↔ ∀ 𝑘 ∈ ( Vtx ‘ ℎ ) ∀ 𝑛 ∈ ( Vtx ‘ ℎ ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 ) )
25 24 cbvabv ⊢ { 𝑔 ∣ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } = { ℎ ∣ ∀ 𝑘 ∈ ( Vtx ‘ ℎ ) ∀ 𝑛 ∈ ( Vtx ‘ ℎ ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ℎ ) 𝑛 ) 𝑝 }
26 17 25 elab2g ⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ { 𝑔 ∣ ∀ 𝑘 ∈ ( Vtx ‘ 𝑔 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝑔 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
27 9 26 bitrid ⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ 𝑣 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 } ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
28 3 27 bitrid ⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )