Metamath Proof Explorer

Theorem isconngr1

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 isconngr1 ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )

Proof

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