Metamath Proof Explorer

Theorem 2pthon3v

Description: For a vertex adjacent to two other vertices there is a simple path of length 2 between these other vertices in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017) (Revised by AV, 24-Jan-2021)

Ref Expression
Hypotheses 2pthon3v.v ⊢V=Vtx⁡G
2pthon3v.e ⊢E=Edg⁡G
Assertion 2pthon3v ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧AB∈E∧BC∈E→∃f∃pfASPathsOn⁡GCp∧f=2

Proof

Step Hyp Ref Expression
1 2pthon3v.v ⊢V=Vtx⁡G
2 2pthon3v.e ⊢E=Edg⁡G
3 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
4 2 3 eqtri ⊢E=ran⁡iEdg⁡G
5 4 eleq2i ⊢AB∈E↔AB∈ran⁡iEdg⁡G
6 eqid ⊢iEdg⁡G=iEdg⁡G
7 1 6 uhgrf ⊢G∈UHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶𝒫V∖∅
8 7 ffnd ⊢G∈UHGraph→iEdg⁡GFndom⁡iEdg⁡G
9 fvelrnb ⊢iEdg⁡GFndom⁡iEdg⁡G→AB∈ran⁡iEdg⁡G↔∃i∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB
10 8 9 syl ⊢G∈UHGraph→AB∈ran⁡iEdg⁡G↔∃i∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB
11 5 10 bitrid ⊢G∈UHGraph→AB∈E↔∃i∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB
12 4 eleq2i ⊢BC∈E↔BC∈ran⁡iEdg⁡G
13 fvelrnb ⊢iEdg⁡GFndom⁡iEdg⁡G→BC∈ran⁡iEdg⁡G↔∃j∈dom⁡iEdg⁡GiEdg⁡G⁡j=BC
14 8 13 syl ⊢G∈UHGraph→BC∈ran⁡iEdg⁡G↔∃j∈dom⁡iEdg⁡GiEdg⁡G⁡j=BC
15 12 14 bitrid ⊢G∈UHGraph→BC∈E↔∃j∈dom⁡iEdg⁡GiEdg⁡G⁡j=BC
16 11 15 anbi12d ⊢G∈UHGraph→AB∈E∧BC∈E↔∃i∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB∧∃j∈dom⁡iEdg⁡GiEdg⁡G⁡j=BC
17 16 adantr ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V→AB∈E∧BC∈E↔∃i∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB∧∃j∈dom⁡iEdg⁡GiEdg⁡G⁡j=BC
18 17 adantr ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→AB∈E∧BC∈E↔∃i∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB∧∃j∈dom⁡iEdg⁡GiEdg⁡G⁡j=BC
19 reeanv ⊢∃i∈dom⁡iEdg⁡G∃j∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC↔∃i∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB∧∃j∈dom⁡iEdg⁡GiEdg⁡G⁡j=BC
20 18 19 bitr4di ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→AB∈E∧BC∈E↔∃i∈dom⁡iEdg⁡G∃j∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC
21 df-s2 ⊢⟨“ij”⟩=⟨“i”⟩++⟨“j”⟩
22 21 ovexi ⊢⟨“ij”⟩∈V
23 df-s3 ⊢⟨“ABC”⟩=⟨“AB”⟩++⟨“C”⟩
24 23 ovexi ⊢⟨“ABC”⟩∈V
25 22 24 pm3.2i ⊢⟨“ij”⟩∈V∧⟨“ABC”⟩∈V
26 eqid ⊢⟨“ABC”⟩=⟨“ABC”⟩
27 eqid ⊢⟨“ij”⟩=⟨“ij”⟩
28 simp-4r ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→A∈V∧B∈V∧C∈V
29 3simpb ⊢A≠B∧A≠C∧B≠C→A≠B∧B≠C
30 29 ad3antlr ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→A≠B∧B≠C
31 eqimss2 ⊢iEdg⁡G⁡i=AB→AB⊆iEdg⁡G⁡i
32 eqimss2 ⊢iEdg⁡G⁡j=BC→BC⊆iEdg⁡G⁡j
33 31 32 anim12i ⊢iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→AB⊆iEdg⁡G⁡i∧BC⊆iEdg⁡G⁡j
34 33 adantl ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→AB⊆iEdg⁡G⁡i∧BC⊆iEdg⁡G⁡j
35 fveqeq2 ⊢i=j→iEdg⁡G⁡i=AB↔iEdg⁡G⁡j=AB
36 35 anbi1d ⊢i=j→iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC↔iEdg⁡G⁡j=AB∧iEdg⁡G⁡j=BC
37 eqtr2 ⊢iEdg⁡G⁡j=AB∧iEdg⁡G⁡j=BC→AB=BC
38 3simpa ⊢A∈V∧B∈V∧C∈V→A∈V∧B∈V
39 3simpc ⊢A∈V∧B∈V∧C∈V→B∈V∧C∈V
40 preq12bg ⊢A∈V∧B∈V∧B∈V∧C∈V→AB=BC↔A=B∧B=C∨A=C∧B=B
41 38 39 40 syl2anc ⊢A∈V∧B∈V∧C∈V→AB=BC↔A=B∧B=C∨A=C∧B=B
42 eqneqall ⊢A=B→A≠B→i≠j
43 42 com12 ⊢A≠B→A=B→i≠j
44 43 3ad2ant1 ⊢A≠B∧A≠C∧B≠C→A=B→i≠j
45 44 com12 ⊢A=B→A≠B∧A≠C∧B≠C→i≠j
46 45 adantr ⊢A=B∧B=C→A≠B∧A≠C∧B≠C→i≠j
47 eqneqall ⊢A=C→A≠C→i≠j
48 47 com12 ⊢A≠C→A=C→i≠j
49 48 3ad2ant2 ⊢A≠B∧A≠C∧B≠C→A=C→i≠j
50 49 com12 ⊢A=C→A≠B∧A≠C∧B≠C→i≠j
51 50 adantr ⊢A=C∧B=B→A≠B∧A≠C∧B≠C→i≠j
52 46 51 jaoi ⊢A=B∧B=C∨A=C∧B=B→A≠B∧A≠C∧B≠C→i≠j
53 41 52 syl6bi ⊢A∈V∧B∈V∧C∈V→AB=BC→A≠B∧A≠C∧B≠C→i≠j
54 53 com23 ⊢A∈V∧B∈V∧C∈V→A≠B∧A≠C∧B≠C→AB=BC→i≠j
55 54 adantl ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V→A≠B∧A≠C∧B≠C→AB=BC→i≠j
56 55 imp ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→AB=BC→i≠j
57 56 com12 ⊢AB=BC→G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→i≠j
58 37 57 syl ⊢iEdg⁡G⁡j=AB∧iEdg⁡G⁡j=BC→G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→i≠j
59 36 58 syl6bi ⊢i=j→iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→i≠j
60 59 com23 ⊢i=j→G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→i≠j
61 2a1 ⊢i≠j→G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→i≠j
62 60 61 pm2.61ine ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→i≠j
63 62 adantr ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G→iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→i≠j
64 63 imp ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→i≠j
65 simplr2 ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G→A≠C
66 65 adantr ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→A≠C
67 26 27 28 30 34 1 6 64 66 2pthond ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→⟨“ij”⟩ASPathsOn⁡GC⟨“ABC”⟩
68 s2len ⊢⟨“ij”⟩=2
69 67 68 jctir ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→⟨“ij”⟩ASPathsOn⁡GC⟨“ABC”⟩∧⟨“ij”⟩=2
70 breq12 ⊢f=⟨“ij”⟩∧p=⟨“ABC”⟩→fASPathsOn⁡GCp↔⟨“ij”⟩ASPathsOn⁡GC⟨“ABC”⟩
71 fveqeq2 ⊢f=⟨“ij”⟩→f=2↔⟨“ij”⟩=2
72 71 adantr ⊢f=⟨“ij”⟩∧p=⟨“ABC”⟩→f=2↔⟨“ij”⟩=2
73 70 72 anbi12d ⊢f=⟨“ij”⟩∧p=⟨“ABC”⟩→fASPathsOn⁡GCp∧f=2↔⟨“ij”⟩ASPathsOn⁡GC⟨“ABC”⟩∧⟨“ij”⟩=2
74 73 spc2egv ⊢⟨“ij”⟩∈V∧⟨“ABC”⟩∈V→⟨“ij”⟩ASPathsOn⁡GC⟨“ABC”⟩∧⟨“ij”⟩=2→∃f∃pfASPathsOn⁡GCp∧f=2
75 25 69 74 mpsyl ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G∧iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→∃f∃pfASPathsOn⁡GCp∧f=2
76 75 ex ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧i∈dom⁡iEdg⁡G∧j∈dom⁡iEdg⁡G→iEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→∃f∃pfASPathsOn⁡GCp∧f=2
77 76 rexlimdvva ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→∃i∈dom⁡iEdg⁡G∃j∈dom⁡iEdg⁡GiEdg⁡G⁡i=AB∧iEdg⁡G⁡j=BC→∃f∃pfASPathsOn⁡GCp∧f=2
78 20 77 sylbid ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C→AB∈E∧BC∈E→∃f∃pfASPathsOn⁡GCp∧f=2
79 78 3impia ⊢G∈UHGraph∧A∈V∧B∈V∧C∈V∧A≠B∧A≠C∧B≠C∧AB∈E∧BC∈E→∃f∃pfASPathsOn⁡GCp∧f=2