Metamath Proof Explorer

Theorem cusconngr

Description: A complete hypergraph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion cusconngr 
|- ( ( G e. UHGraph /\ G e. ComplGraph ) -> G e. ConnGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 iscplgredg 
 |-  ( G e. UHGraph -> ( G e. ComplGraph <-> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. e e. ( Edg ` G ) { k , n } C_ e ) )
4 simp-4l 
 |-  ( ( ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) /\ e e. ( Edg ` G ) ) /\ { k , n } C_ e ) -> G e. UHGraph )
5 simpr 
 |-  ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) -> k e. ( Vtx ` G ) )
6 eldifi 
 |-  ( n e. ( ( Vtx ` G ) \ { k } ) -> n e. ( Vtx ` G ) )
7 5 6 anim12i 
 |-  ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) -> ( k e. ( Vtx ` G ) /\ n e. ( Vtx ` G ) ) )
8 7 adantr 
 |-  ( ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) /\ e e. ( Edg ` G ) ) -> ( k e. ( Vtx ` G ) /\ n e. ( Vtx ` G ) ) )
9 8 adantr 
 |-  ( ( ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) /\ e e. ( Edg ` G ) ) /\ { k , n } C_ e ) -> ( k e. ( Vtx ` G ) /\ n e. ( Vtx ` G ) ) )
10 id 
 |-  ( e e. ( Edg ` G ) -> e e. ( Edg ` G ) )
11 sseq2 
 |-  ( c = e -> ( { k , n } C_ c <-> { k , n } C_ e ) )
12 11 adantl 
 |-  ( ( e e. ( Edg ` G ) /\ c = e ) -> ( { k , n } C_ c <-> { k , n } C_ e ) )
13 10 12 rspcedv 
 |-  ( e e. ( Edg ` G ) -> ( { k , n } C_ e -> E. c e. ( Edg ` G ) { k , n } C_ c ) )
14 13 adantl 
 |-  ( ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) /\ e e. ( Edg ` G ) ) -> ( { k , n } C_ e -> E. c e. ( Edg ` G ) { k , n } C_ c ) )
15 14 imp 
 |-  ( ( ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) /\ e e. ( Edg ` G ) ) /\ { k , n } C_ e ) -> E. c e. ( Edg ` G ) { k , n } C_ c )
16 1 2 1pthon2v 
 |-  ( ( G e. UHGraph /\ ( k e. ( Vtx ` G ) /\ n e. ( Vtx ` G ) ) /\ E. c e. ( Edg ` G ) { k , n } C_ c ) -> E. f E. p f ( k ( PathsOn ` G ) n ) p )
17 4 9 15 16 syl3anc 
 |-  ( ( ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) /\ e e. ( Edg ` G ) ) /\ { k , n } C_ e ) -> E. f E. p f ( k ( PathsOn ` G ) n ) p )
18 17 rexlimdva2 
 |-  ( ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) /\ n e. ( ( Vtx ` G ) \ { k } ) ) -> ( E. e e. ( Edg ` G ) { k , n } C_ e -> E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
19 18 ralimdva 
 |-  ( ( G e. UHGraph /\ k e. ( Vtx ` G ) ) -> ( A. n e. ( ( Vtx ` G ) \ { k } ) E. e e. ( Edg ` G ) { k , n } C_ e -> A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
20 19 ralimdva 
 |-  ( G e. UHGraph -> ( A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. e e. ( Edg ` G ) { k , n } C_ e -> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
21 3 20 sylbid 
 |-  ( G e. UHGraph -> ( G e. ComplGraph -> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
22 21 imp 
 |-  ( ( G e. UHGraph /\ G e. ComplGraph ) -> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p )
23 1 isconngr1 
 |-  ( G e. UHGraph -> ( G e. ConnGraph <-> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
24 23 adantr 
 |-  ( ( G e. UHGraph /\ G e. ComplGraph ) -> ( G e. ConnGraph <-> A. k e. ( Vtx ` G ) A. n e. ( ( Vtx ` G ) \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
25 22 24 mpbird 
 |-  ( ( G e. UHGraph /\ G e. ComplGraph ) -> G e. ConnGraph )