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