Metamath Proof Explorer

Theorem 1pthon2ve

Description: For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 22-Jan-2021) (Proof shortened by AV, 15-Feb-2021)

Ref Expression
Hypotheses 1pthon2v.v ⊢ V = Vtx ⁡ G
1pthon2v.e ⊢ E = Edg ⁡ G
Assertion 1pthon2ve ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A B ∈ E → ∃ f ∃ p f A PathsOn ⁡ G B p

Proof

Step Hyp Ref Expression
1 1pthon2v.v ⊢ V = Vtx ⁡ G
2 1pthon2v.e ⊢ E = Edg ⁡ G
3 id ⊢ A B ∈ E → A B ∈ E
4 sseq2 ⊢ e = A B → A B ⊆ e ↔ A B ⊆ A B
5 4 adantl ⊢ A B ∈ E ∧ e = A B → A B ⊆ e ↔ A B ⊆ A B
6 ssidd ⊢ A B ∈ E → A B ⊆ A B
7 3 5 6 rspcedvd ⊢ A B ∈ E → ∃ e ∈ E A B ⊆ e
8 1 2 1pthon2v ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ ∃ e ∈ E A B ⊆ e → ∃ f ∃ p f A PathsOn ⁡ G B p
9 7 8 syl3an3 ⊢ G ∈ UHGraph ∧ A ∈ V ∧ B ∈ V ∧ A B ∈ E → ∃ f ∃ p f A PathsOn ⁡ G B p