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 A B E B C E f p f A SPathsOn G C p 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 A B E A B 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 G Fn dom iEdg G
9 fvelrnb iEdg G Fn dom iEdg G A B ran iEdg G i dom iEdg G iEdg G i = A B
10 8 9 syl G UHGraph A B ran iEdg G i dom iEdg G iEdg G i = A B
11 5 10 syl5bb G UHGraph A B E i dom iEdg G iEdg G i = A B
12 4 eleq2i B C E B C ran iEdg G
13 fvelrnb iEdg G Fn dom iEdg G B C ran iEdg G j dom iEdg G iEdg G j = B C
14 8 13 syl G UHGraph B C ran iEdg G j dom iEdg G iEdg G j = B C
15 12 14 syl5bb G UHGraph B C E j dom iEdg G iEdg G j = B C
16 11 15 anbi12d G UHGraph A B E B C E i dom iEdg G iEdg G i = A B j dom iEdg G iEdg G j = B C
17 16 adantr G UHGraph A V B V C V A B E B C E i dom iEdg G iEdg G i = A B j dom iEdg G iEdg G j = B C
18 17 adantr G UHGraph A V B V C V A B A C B C A B E B C E i dom iEdg G iEdg G i = A B j dom iEdg G iEdg G j = B C
19 reeanv i dom iEdg G j dom iEdg G iEdg G i = A B iEdg G j = B C i dom iEdg G iEdg G i = A B j dom iEdg G iEdg G j = B C
20 18 19 bitr4di G UHGraph A V B V C V A B A C B C A B E B C E i dom iEdg G j dom iEdg G iEdg G i = A B iEdg G j = B C
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 = A B iEdg G j = B C 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 = A B iEdg G j = B C A B B C
31 eqimss2 iEdg G i = A B A B iEdg G i
32 eqimss2 iEdg G j = B C B C iEdg G j
33 31 32 anim12i iEdg G i = A B iEdg G j = B C A B iEdg G i B C 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 = A B iEdg G j = B C A B iEdg G i B C iEdg G j
35 fveqeq2 i = j iEdg G i = A B iEdg G j = A B
36 35 anbi1d i = j iEdg G i = A B iEdg G j = B C iEdg G j = A B iEdg G j = B C
37 eqtr2 iEdg G j = A B iEdg G j = B C A B = B C
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 A B = B C A = B B = C A = C B = B
41 38 39 40 syl2anc A V B V C V A B = B C 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 A B = B C A B A C B C i j
54 53 com23 A V B V C V A B A C B C A B = B C i j
55 54 adantl G UHGraph A V B V C V A B A C B C A B = B C i j
56 55 imp G UHGraph A V B V C V A B A C B C A B = B C i j
57 56 com12 A B = B C G UHGraph A V B V C V A B A C B C i j
58 37 57 syl iEdg G j = A B iEdg G j = B C 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 = A B iEdg G j = B C 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 = A B iEdg G j = B C i j
61 2a1 i j G UHGraph A V B V C V A B A C B C iEdg G i = A B iEdg G j = B C i j
62 60 61 pm2.61ine G UHGraph A V B V C V A B A C B C iEdg G i = A B iEdg G j = B C 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 = A B iEdg G j = B C 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 = A B iEdg G j = B C 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 = A B iEdg G j = B C 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 = A B iEdg G j = B C ⟨“ ij ”⟩ A SPathsOn G C ⟨“ 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 = A B iEdg G j = B C ⟨“ ij ”⟩ A SPathsOn G C ⟨“ ABC ”⟩ ⟨“ ij ”⟩ = 2
70 breq12 f = ⟨“ ij ”⟩ p = ⟨“ ABC ”⟩ f A SPathsOn G C p ⟨“ ij ”⟩ A SPathsOn G C ⟨“ 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 ”⟩ f A SPathsOn G C p f = 2 ⟨“ ij ”⟩ A SPathsOn G C ⟨“ ABC ”⟩ ⟨“ ij ”⟩ = 2
74 73 spc2egv ⟨“ ij ”⟩ V ⟨“ ABC ”⟩ V ⟨“ ij ”⟩ A SPathsOn G C ⟨“ ABC ”⟩ ⟨“ ij ”⟩ = 2 f p f A SPathsOn G C p 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 = A B iEdg G j = B C f p f A SPathsOn G C p 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 = A B iEdg G j = B C f p f A SPathsOn G C p 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 G iEdg G i = A B iEdg G j = B C f p f A SPathsOn G C p f = 2
78 20 77 sylbid G UHGraph A V B V C V A B A C B C A B E B C E f p f A SPathsOn G C p f = 2
79 78 3impia G UHGraph A V B V C V A B A C B C A B E B C E f p f A SPathsOn G C p f = 2