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 = { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p }

Proof

Step Hyp Ref Expression
1 df-conngr 
 |-  ConnGraph = { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p }
2 eqid 
 |-  ( Vtx ` g ) = ( Vtx ` g )
3 2 0pthonv 
 |-  ( k e. ( Vtx ` g ) -> E. f E. p f ( k ( PathsOn ` g ) k ) p )
4 oveq2 
 |-  ( n = k -> ( k ( PathsOn ` g ) n ) = ( k ( PathsOn ` g ) k ) )
5 4 breqd 
 |-  ( n = k -> ( f ( k ( PathsOn ` g ) n ) p <-> f ( k ( PathsOn ` g ) k ) p ) )
6 5 2exbidv 
 |-  ( n = k -> ( E. f E. p f ( k ( PathsOn ` g ) n ) p <-> E. f E. p f ( k ( PathsOn ` g ) k ) p ) )
7 6 ralsng 
 |-  ( k e. ( Vtx ` g ) -> ( A. n e. { k } E. f E. p f ( k ( PathsOn ` g ) n ) p <-> E. f E. p f ( k ( PathsOn ` g ) k ) p ) )
8 3 7 mpbird 
 |-  ( k e. ( Vtx ` g ) -> A. n e. { k } E. f E. p f ( k ( PathsOn ` g ) n ) p )
9 difsnid 
 |-  ( k e. ( Vtx ` g ) -> ( ( ( Vtx ` g ) \ { k } ) u. { k } ) = ( Vtx ` g ) )
10 9 eqcomd 
 |-  ( k e. ( Vtx ` g ) -> ( Vtx ` g ) = ( ( ( Vtx ` g ) \ { k } ) u. { k } ) )
11 10 raleqdv 
 |-  ( k e. ( Vtx ` g ) -> ( A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. n e. ( ( ( Vtx ` g ) \ { k } ) u. { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
12 ralunb 
 |-  ( A. n e. ( ( ( Vtx ` g ) \ { k } ) u. { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> ( A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p /\ A. n e. { k } E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
13 11 12 bitrdi 
 |-  ( k e. ( Vtx ` g ) -> ( A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> ( A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p /\ A. n e. { k } E. f E. p f ( k ( PathsOn ` g ) n ) p ) ) )
14 8 13 mpbiran2d 
 |-  ( k e. ( Vtx ` g ) -> ( A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
15 14 ralbiia 
 |-  ( A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p )
16 fvex 
 |-  ( Vtx ` g ) e. _V
17 raleq 
 |-  ( v = ( Vtx ` g ) -> ( A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
18 17 raleqbi1dv 
 |-  ( v = ( Vtx ` g ) -> ( A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
19 difeq1 
 |-  ( v = ( Vtx ` g ) -> ( v \ { k } ) = ( ( Vtx ` g ) \ { k } ) )
20 19 raleqdv 
 |-  ( v = ( Vtx ` g ) -> ( A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
21 20 raleqbi1dv 
 |-  ( v = ( Vtx ` g ) -> ( A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
22 18 21 bibi12d 
 |-  ( v = ( Vtx ` g ) -> ( ( A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) <-> ( A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) ) )
23 16 22 sbcie 
 |-  ( [. ( Vtx ` g ) / v ]. ( A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) <-> ( A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` g ) A. n e. ( ( Vtx ` g ) \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
24 15 23 mpbir 
 |-  [. ( Vtx ` g ) / v ]. ( A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p )
25 sbcbi1 
 |-  ( [. ( Vtx ` g ) / v ]. ( A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) -> ( [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> [. ( Vtx ` g ) / v ]. A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
26 24 25 ax-mp 
 |-  ( [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> [. ( Vtx ` g ) / v ]. A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p )
27 26 abbii 
 |-  { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p } = { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p }
28 1 27 eqtri 
 |-  ConnGraph = { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( PathsOn ` g ) n ) p }