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 ( ( 𝐺 ∈ UHGraph ∧ 𝐺 ∈ ComplGraph ) → 𝐺 ∈ ConnGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 iscplgredg ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑒 ) )
4 simp-4l ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑘 , 𝑛 } ⊆ 𝑒 ) → 𝐺 ∈ UHGraph )
5 simpr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑘 ∈ ( Vtx ‘ 𝐺 ) )
6 eldifi ⊢ ( 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) → 𝑛 ∈ ( Vtx ‘ 𝐺 ) )
7 5 6 anim12i ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) → ( 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ) )
8 7 adantr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ) )
9 8 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑘 , 𝑛 } ⊆ 𝑒 ) → ( 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ) )
10 id ⊢ ( 𝑒 ∈ ( Edg ‘ 𝐺 ) → 𝑒 ∈ ( Edg ‘ 𝐺 ) )
11 sseq2 ⊢ ( 𝑐 = 𝑒 → ( { 𝑘 , 𝑛 } ⊆ 𝑐 ↔ { 𝑘 , 𝑛 } ⊆ 𝑒 ) )
12 11 adantl ⊢ ( ( 𝑒 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑐 = 𝑒 ) → ( { 𝑘 , 𝑛 } ⊆ 𝑐 ↔ { 𝑘 , 𝑛 } ⊆ 𝑒 ) )
13 10 12 rspcedv ⊢ ( 𝑒 ∈ ( Edg ‘ 𝐺 ) → ( { 𝑘 , 𝑛 } ⊆ 𝑒 → ∃ 𝑐 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑐 ) )
14 13 adantl ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑘 , 𝑛 } ⊆ 𝑒 → ∃ 𝑐 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑐 ) )
15 14 imp ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑘 , 𝑛 } ⊆ 𝑒 ) → ∃ 𝑐 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑐 )
16 1 2 1pthon2v ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ∃ 𝑐 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑐 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
17 4 9 15 16 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑘 , 𝑛 } ⊆ 𝑒 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
18 17 rexlimdva2 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑒 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
19 18 ralimdva ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑒 → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
20 19 ralimdva ⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑘 , 𝑛 } ⊆ 𝑒 → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
21 3 20 sylbid ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ∈ ComplGraph → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
22 21 imp ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐺 ∈ ComplGraph ) → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
23 1 isconngr1 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
24 23 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐺 ∈ ComplGraph ) → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
25 22 24 mpbird ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐺 ∈ ComplGraph ) → 𝐺 ∈ ConnGraph )