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 UHGraph G ComplGraph G ConnGraph

Proof

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