This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
		1pthon2v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	Assertion	1pthon2ve	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 )

Proof

Step	Hyp	Ref	Expression
1		1pthon2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		1pthon2v.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		id	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 → { 𝐴 , 𝐵 } ∈ 𝐸 )
4		sseq2	⊢ ( 𝑒 = { 𝐴 , 𝐵 } → ( { 𝐴 , 𝐵 } ⊆ 𝑒 ↔ { 𝐴 , 𝐵 } ⊆ { 𝐴 , 𝐵 } ) )
5	4	adantl	⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ 𝑒 = { 𝐴 , 𝐵 } ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 ↔ { 𝐴 , 𝐵 } ⊆ { 𝐴 , 𝐵 } ) )
6		ssidd	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 → { 𝐴 , 𝐵 } ⊆ { 𝐴 , 𝐵 } )
7	3 5 6	rspcedvd	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐸 → ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 )
8	1 2	1pthon2v	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 )
9	7 8	syl3an3	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 )