This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Examples for walks, trails and paths 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