Metamath Proof Explorer

Theorem 1pthon2v

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)

Ref Expression
Hypotheses 1pthon2v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
1pthon2v.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion 1pthon2v ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 )

Proof

Step Hyp Ref Expression
1 1pthon2v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1pthon2v.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
4 3 anim2i ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐴 ∈ 𝑉 ) )
5 4 3adant3 ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ( 𝐺 ∈ UHGraph ∧ 𝐴 ∈ 𝑉 ) )
6 5 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐴 ∈ 𝑉 ) )
7 1 0pthonv ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) 𝑝 )
8 6 7 simpl2im ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) 𝑝 )
9 oveq2 ⊢ ( 𝐵 = 𝐴 → ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) = ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) )
10 9 eqcoms ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) = ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) )
11 10 breqd ⊢ ( 𝐴 = 𝐵 → ( 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ↔ 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) 𝑝 ) )
12 11 2exbidv ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) 𝑝 ) )
13 12 adantr ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐴 ) 𝑝 ) )
14 8 13 mpbird ⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 )
15 14 ex ⊢ ( 𝐴 = 𝐵 → ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) )
16 2 eleq2i ⊢ ( 𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
17 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
18 17 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( 𝑒 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
19 16 18 syl5bb ⊢ ( 𝐺 ∈ UHGraph → ( 𝑒 ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑒 ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
21 s1cli ⊢ ⟨“ 𝑖 ”⟩ ∈ Word V
22 s2cli ⊢ ⟨“ 𝐴 𝐵 ”⟩ ∈ Word V
23 21 22 pm3.2i ⊢ ( ⟨“ 𝑖 ”⟩ ∈ Word V ∧ ⟨“ 𝐴 𝐵 ”⟩ ∈ Word V )
24 eqid ⊢ ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐴 𝐵 ”⟩
25 eqid ⊢ ⟨“ 𝑖 ”⟩ = ⟨“ 𝑖 ”⟩
26 simpl2l ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → 𝐴 ∈ 𝑉 )
27 simpl2r ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → 𝐵 ∈ 𝑉 )
28 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 } ) )
29 28 com12 ⊢ ( 𝐴 ≠ 𝐵 → ( 𝐴 = 𝐵 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 } ) )
30 29 3ad2ant3 ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐵 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 } ) )
31 30 adantr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → ( 𝐴 = 𝐵 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 } ) )
32 31 imp ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) ∧ 𝐴 = 𝐵 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = { 𝐴 } )
33 sseq2 ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 ↔ { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
34 33 adantl ⊢ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 ↔ { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
35 34 biimpa ⊢ ( ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) → { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
36 35 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
37 36 adantr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
38 24 25 26 27 32 37 1 17 1pthond ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → ⟨“ 𝑖 ”⟩ ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) ⟨“ 𝐴 𝐵 ”⟩ )
39 breq12 ⊢ ( ( 𝑓 = ⟨“ 𝑖 ”⟩ ∧ 𝑝 = ⟨“ 𝐴 𝐵 ”⟩ ) → ( 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ↔ ⟨“ 𝑖 ”⟩ ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) ⟨“ 𝐴 𝐵 ”⟩ ) )
40 39 spc2egv ⊢ ( ( ⟨“ 𝑖 ”⟩ ∈ Word V ∧ ⟨“ 𝐴 𝐵 ”⟩ ∈ Word V ) → ( ⟨“ 𝑖 ”⟩ ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) ⟨“ 𝐴 𝐵 ”⟩ → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) )
41 23 38 40 mpsyl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∧ { 𝐴 , 𝐵 } ⊆ 𝑒 ) ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 )
42 41 exp44 ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) ) ) )
43 42 rexlimdv ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) ) )
44 20 43 sylbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑒 ∈ 𝐸 → ( { 𝐴 , 𝐵 } ⊆ 𝑒 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) ) )
45 44 rexlimdv ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) )
46 45 3exp ⊢ ( 𝐺 ∈ UHGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐵 → ( ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) ) ) )
47 46 com34 ⊢ ( 𝐺 ∈ UHGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 → ( 𝐴 ≠ 𝐵 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) ) ) )
48 47 3imp ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ( 𝐴 ≠ 𝐵 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) )
49 48 com12 ⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 ) )
50 15 49 pm2.61ine ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝐴 , 𝐵 } ⊆ 𝑒 ) → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐵 ) 𝑝 )