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 ⊢V=Vtx⁡G
1pthon2v.e ⊢E=Edg⁡G
Assertion 1pthon2v ⊢G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp

Proof

Step Hyp Ref Expression
1 1pthon2v.v ⊢V=Vtx⁡G
2 1pthon2v.e ⊢E=Edg⁡G
3 simpl ⊢A∈V∧B∈V→A∈V
4 3 anim2i ⊢G∈UHGraph∧A∈V∧B∈V→G∈UHGraph∧A∈V
5 4 3adant3 ⊢G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→G∈UHGraph∧A∈V
6 5 adantl ⊢A=B∧G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→G∈UHGraph∧A∈V
7 1 0pthonv ⊢A∈V→∃f∃pfAPathsOn⁡GAp
8 6 7 simpl2im ⊢A=B∧G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GAp
9 oveq2 ⊢B=A→APathsOn⁡GB=APathsOn⁡GA
10 9 eqcoms ⊢A=B→APathsOn⁡GB=APathsOn⁡GA
11 10 breqd ⊢A=B→fAPathsOn⁡GBp↔fAPathsOn⁡GAp
12 11 2exbidv ⊢A=B→∃f∃pfAPathsOn⁡GBp↔∃f∃pfAPathsOn⁡GAp
13 12 adantr ⊢A=B∧G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp↔∃f∃pfAPathsOn⁡GAp
14 8 13 mpbird ⊢A=B∧G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp
15 14 ex ⊢A=B→G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp
16 2 eleq2i ⊢e∈E↔e∈Edg⁡G
17 eqid ⊢iEdg⁡G=iEdg⁡G
18 17 uhgredgiedgb ⊢G∈UHGraph→e∈Edg⁡G↔∃i∈dom⁡iEdg⁡Ge=iEdg⁡G⁡i
19 16 18 bitrid ⊢G∈UHGraph→e∈E↔∃i∈dom⁡iEdg⁡Ge=iEdg⁡G⁡i
20 19 3ad2ant1 ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B→e∈E↔∃i∈dom⁡iEdg⁡Ge=iEdg⁡G⁡i
21 s1cli ⊢⟨“i”⟩∈WordV
22 s2cli ⊢⟨“AB”⟩∈WordV
23 21 22 pm3.2i ⊢⟨“i”⟩∈WordV∧⟨“AB”⟩∈WordV
24 eqid ⊢⟨“AB”⟩=⟨“AB”⟩
25 eqid ⊢⟨“i”⟩=⟨“i”⟩
26 simpl2l ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e→A∈V
27 simpl2r ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e→B∈V
28 eqneqall ⊢A=B→A≠B→iEdg⁡G⁡i=A
29 28 com12 ⊢A≠B→A=B→iEdg⁡G⁡i=A
30 29 3ad2ant3 ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B→A=B→iEdg⁡G⁡i=A
31 30 adantr ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e→A=B→iEdg⁡G⁡i=A
32 31 imp ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e∧A=B→iEdg⁡G⁡i=A
33 sseq2 ⊢e=iEdg⁡G⁡i→AB⊆e↔AB⊆iEdg⁡G⁡i
34 33 adantl ⊢i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i→AB⊆e↔AB⊆iEdg⁡G⁡i
35 34 biimpa ⊢i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e→AB⊆iEdg⁡G⁡i
36 35 adantl ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e→AB⊆iEdg⁡G⁡i
37 36 adantr ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e∧A≠B→AB⊆iEdg⁡G⁡i
38 24 25 26 27 32 37 1 17 1pthond ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e→⟨“i”⟩APathsOn⁡GB⟨“AB”⟩
39 breq12 ⊢f=⟨“i”⟩∧p=⟨“AB”⟩→fAPathsOn⁡GBp↔⟨“i”⟩APathsOn⁡GB⟨“AB”⟩
40 39 spc2egv ⊢⟨“i”⟩∈WordV∧⟨“AB”⟩∈WordV→⟨“i”⟩APathsOn⁡GB⟨“AB”⟩→∃f∃pfAPathsOn⁡GBp
41 23 38 40 mpsyl ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B∧i∈dom⁡iEdg⁡G∧e=iEdg⁡G⁡i∧AB⊆e→∃f∃pfAPathsOn⁡GBp
42 41 exp44 ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B→i∈dom⁡iEdg⁡G→e=iEdg⁡G⁡i→AB⊆e→∃f∃pfAPathsOn⁡GBp
43 42 rexlimdv ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B→∃i∈dom⁡iEdg⁡Ge=iEdg⁡G⁡i→AB⊆e→∃f∃pfAPathsOn⁡GBp
44 20 43 sylbid ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B→e∈E→AB⊆e→∃f∃pfAPathsOn⁡GBp
45 44 rexlimdv ⊢G∈UHGraph∧A∈V∧B∈V∧A≠B→∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp
46 45 3exp ⊢G∈UHGraph→A∈V∧B∈V→A≠B→∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp
47 46 com34 ⊢G∈UHGraph→A∈V∧B∈V→∃e∈EAB⊆e→A≠B→∃f∃pfAPathsOn⁡GBp
48 47 3imp ⊢G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→A≠B→∃f∃pfAPathsOn⁡GBp
49 48 com12 ⊢A≠B→G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp
50 15 49 pm2.61ine ⊢G∈UHGraph∧A∈V∧B∈V∧∃e∈EAB⊆e→∃f∃pfAPathsOn⁡GBp