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⁡Gkn⊆e
4 simp-4l ⊢G∈UHGraph∧k∈Vtx⁡G∧n∈Vtx⁡G∖k∧e∈Edg⁡G∧kn⊆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∧kn⊆e→k∈Vtx⁡G∧n∈Vtx⁡G
10 id ⊢e∈Edg⁡G→e∈Edg⁡G
11 sseq2 ⊢c=e→kn⊆c↔kn⊆e
12 11 adantl ⊢e∈Edg⁡G∧c=e→kn⊆c↔kn⊆e
13 10 12 rspcedv ⊢e∈Edg⁡G→kn⊆e→∃c∈Edg⁡Gkn⊆c
14 13 adantl ⊢G∈UHGraph∧k∈Vtx⁡G∧n∈Vtx⁡G∖k∧e∈Edg⁡G→kn⊆e→∃c∈Edg⁡Gkn⊆c
15 14 imp ⊢G∈UHGraph∧k∈Vtx⁡G∧n∈Vtx⁡G∖k∧e∈Edg⁡G∧kn⊆e→∃c∈Edg⁡Gkn⊆c
16 1 2 1pthon2v ⊢G∈UHGraph∧k∈Vtx⁡G∧n∈Vtx⁡G∧∃c∈Edg⁡Gkn⊆c→∃f∃pfkPathsOn⁡Gnp
17 4 9 15 16 syl3anc ⊢G∈UHGraph∧k∈Vtx⁡G∧n∈Vtx⁡G∖k∧e∈Edg⁡G∧kn⊆e→∃f∃pfkPathsOn⁡Gnp
18 17 rexlimdva2 ⊢G∈UHGraph∧k∈Vtx⁡G∧n∈Vtx⁡G∖k→∃e∈Edg⁡Gkn⊆e→∃f∃pfkPathsOn⁡Gnp
19 18 ralimdva ⊢G∈UHGraph∧k∈Vtx⁡G→∀n∈Vtx⁡G∖k∃e∈Edg⁡Gkn⊆e→∀n∈Vtx⁡G∖k∃f∃pfkPathsOn⁡Gnp
20 19 ralimdva ⊢G∈UHGraph→∀k∈Vtx⁡G∀n∈Vtx⁡G∖k∃e∈Edg⁡Gkn⊆e→∀k∈Vtx⁡G∀n∈Vtx⁡G∖k∃f∃pfkPathsOn⁡Gnp
21 3 20 sylbid ⊢G∈UHGraph→G∈ComplGraph→∀k∈Vtx⁡G∀n∈Vtx⁡G∖k∃f∃pfkPathsOn⁡Gnp
22 21 imp ⊢G∈UHGraph∧G∈ComplGraph→∀k∈Vtx⁡G∀n∈Vtx⁡G∖k∃f∃pfkPathsOn⁡Gnp
23 1 isconngr1 ⊢G∈UHGraph→G∈ConnGraph↔∀k∈Vtx⁡G∀n∈Vtx⁡G∖k∃f∃pfkPathsOn⁡Gnp
24 23 adantr ⊢G∈UHGraph∧G∈ComplGraph→G∈ConnGraph↔∀k∈Vtx⁡G∀n∈Vtx⁡G∖k∃f∃pfkPathsOn⁡Gnp
25 22 24 mpbird ⊢G∈UHGraph∧G∈ComplGraph→G∈ConnGraph