Metamath Proof Explorer

Theorem dfconngr1

Description: Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion dfconngr1 ConnGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑛 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝑔 ) 𝑛 ) 𝑝 }

Proof

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 ‘ 𝑔 ) 𝑛 ) 𝑝 }