Metamath Proof Explorer

Theorem 1conngr

Description: A graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion 1conngr 
|- ( ( G e. W /\ ( Vtx ` G ) = { N } ) -> G e. ConnGraph )

Proof

Step Hyp Ref Expression
1 snidg 
 |-  ( N e. _V -> N e. { N } )
2 1 adantr 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> N e. { N } )
3 eleq2 
 |-  ( ( Vtx ` G ) = { N } -> ( N e. ( Vtx ` G ) <-> N e. { N } ) )
4 3 ad2antll 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> ( N e. ( Vtx ` G ) <-> N e. { N } ) )
5 2 4 mpbird 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> N e. ( Vtx ` G ) )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 6 0pthonv 
 |-  ( N e. ( Vtx ` G ) -> E. f E. p f ( N ( PathsOn ` G ) N ) p )
8 5 7 syl 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> E. f E. p f ( N ( PathsOn ` G ) N ) p )
9 oveq2 
 |-  ( n = N -> ( N ( PathsOn ` G ) n ) = ( N ( PathsOn ` G ) N ) )
10 9 breqd 
 |-  ( n = N -> ( f ( N ( PathsOn ` G ) n ) p <-> f ( N ( PathsOn ` G ) N ) p ) )
11 10 2exbidv 
 |-  ( n = N -> ( E. f E. p f ( N ( PathsOn ` G ) n ) p <-> E. f E. p f ( N ( PathsOn ` G ) N ) p ) )
12 11 ralsng 
 |-  ( N e. _V -> ( A. n e. { N } E. f E. p f ( N ( PathsOn ` G ) n ) p <-> E. f E. p f ( N ( PathsOn ` G ) N ) p ) )
13 12 adantr 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> ( A. n e. { N } E. f E. p f ( N ( PathsOn ` G ) n ) p <-> E. f E. p f ( N ( PathsOn ` G ) N ) p ) )
14 8 13 mpbird 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> A. n e. { N } E. f E. p f ( N ( PathsOn ` G ) n ) p )
15 oveq1 
 |-  ( k = N -> ( k ( PathsOn ` G ) n ) = ( N ( PathsOn ` G ) n ) )
16 15 breqd 
 |-  ( k = N -> ( f ( k ( PathsOn ` G ) n ) p <-> f ( N ( PathsOn ` G ) n ) p ) )
17 16 2exbidv 
 |-  ( k = N -> ( E. f E. p f ( k ( PathsOn ` G ) n ) p <-> E. f E. p f ( N ( PathsOn ` G ) n ) p ) )
18 17 ralbidv 
 |-  ( k = N -> ( A. n e. { N } E. f E. p f ( k ( PathsOn ` G ) n ) p <-> A. n e. { N } E. f E. p f ( N ( PathsOn ` G ) n ) p ) )
19 18 ralsng 
 |-  ( N e. _V -> ( A. k e. { N } A. n e. { N } E. f E. p f ( k ( PathsOn ` G ) n ) p <-> A. n e. { N } E. f E. p f ( N ( PathsOn ` G ) n ) p ) )
20 19 adantr 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> ( A. k e. { N } A. n e. { N } E. f E. p f ( k ( PathsOn ` G ) n ) p <-> A. n e. { N } E. f E. p f ( N ( PathsOn ` G ) n ) p ) )
21 14 20 mpbird 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> A. k e. { N } A. n e. { N } E. f E. p f ( k ( PathsOn ` G ) n ) p )
22 raleq 
 |-  ( ( Vtx ` G ) = { N } -> ( A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p <-> A. n e. { N } E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
23 22 raleqbi1dv 
 |-  ( ( Vtx ` G ) = { N } -> ( A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p <-> A. k e. { N } A. n e. { N } E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
24 23 ad2antll 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> ( A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p <-> A. k e. { N } A. n e. { N } E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
25 21 24 mpbird 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p )
26 6 isconngr 
 |-  ( G e. W -> ( G e. ConnGraph <-> A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
27 26 ad2antrl 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> ( G e. ConnGraph <-> A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
28 25 27 mpbird 
 |-  ( ( N e. _V /\ ( G e. W /\ ( Vtx ` G ) = { N } ) ) -> G e. ConnGraph )
29 28 ex 
 |-  ( N e. _V -> ( ( G e. W /\ ( Vtx ` G ) = { N } ) -> G e. ConnGraph ) )
30 snprc 
 |-  ( -. N e. _V <-> { N } = (/) )
31 eqeq2 
 |-  ( { N } = (/) -> ( ( Vtx ` G ) = { N } <-> ( Vtx ` G ) = (/) ) )
32 31 anbi2d 
 |-  ( { N } = (/) -> ( ( G e. W /\ ( Vtx ` G ) = { N } ) <-> ( G e. W /\ ( Vtx ` G ) = (/) ) ) )
33 0vconngr 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> G e. ConnGraph )
34 32 33 syl6bi 
 |-  ( { N } = (/) -> ( ( G e. W /\ ( Vtx ` G ) = { N } ) -> G e. ConnGraph ) )
35 30 34 sylbi 
 |-  ( -. N e. _V -> ( ( G e. W /\ ( Vtx ` G ) = { N } ) -> G e. ConnGraph ) )
36 29 35 pm2.61i 
 |-  ( ( G e. W /\ ( Vtx ` G ) = { N } ) -> G e. ConnGraph )