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 e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( { A , B } e. E /\ { B , C } e. E ) ) -> E. f E. 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. E <-> { A , B } e. ran ( iEdg ` G ) )
6 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
7 1 6 uhgrf 
 |-  ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
8 7 ffnd 
 |-  ( G e. UHGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
9 fvelrnb 
 |-  ( ( iEdg ` G ) Fn dom ( iEdg ` G ) -> ( { A , B } e. ran ( iEdg ` G ) <-> E. i e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` i ) = { A , B } ) )
10 8 9 syl 
 |-  ( G e. UHGraph -> ( { A , B } e. ran ( iEdg ` G ) <-> E. i e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` i ) = { A , B } ) )
11 5 10 syl5bb 
 |-  ( G e. UHGraph -> ( { A , B } e. E <-> E. i e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` i ) = { A , B } ) )
12 4 eleq2i 
 |-  ( { B , C } e. E <-> { B , C } e. ran ( iEdg ` G ) )
13 fvelrnb 
 |-  ( ( iEdg ` G ) Fn dom ( iEdg ` G ) -> ( { B , C } e. ran ( iEdg ` G ) <-> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { B , C } ) )
14 8 13 syl 
 |-  ( G e. UHGraph -> ( { B , C } e. ran ( iEdg ` G ) <-> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { B , C } ) )
15 12 14 syl5bb 
 |-  ( G e. UHGraph -> ( { B , C } e. E <-> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { B , C } ) )
16 11 15 anbi12d 
 |-  ( G e. UHGraph -> ( ( { A , B } e. E /\ { B , C } e. E ) <-> ( E. i e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` i ) = { A , B } /\ E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { B , C } ) ) )
17 16 adantr 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( { A , B } e. E /\ { B , C } e. E ) <-> ( E. i e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` i ) = { A , B } /\ E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { B , C } ) ) )
18 17 adantr 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( { A , B } e. E /\ { B , C } e. E ) <-> ( E. i e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` i ) = { A , B } /\ E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { B , C } ) ) )
19 reeanv 
 |-  ( E. i e. dom ( iEdg ` G ) E. j e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) <-> ( E. i e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` i ) = { A , B } /\ E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = { B , C } ) )
20 18 19 bitr4di 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( { A , B } e. E /\ { B , C } e. E ) <-> E. i e. dom ( iEdg ` G ) E. j e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) ) )
21 df-s2 
 |-  <" i j "> = ( <" i "> ++ <" j "> )
22 21 ovexi 
 |-  <" i j "> e. _V
23 df-s3 
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
24 23 ovexi 
 |-  <" A B C "> e. _V
25 22 24 pm3.2i 
 |-  ( <" i j "> e. _V /\ <" A B C "> e. _V )
26 eqid 
 |-  <" A B C "> = <" A B C ">
27 eqid 
 |-  <" i j "> = <" i j ">
28 simp-4r 
 |-  ( ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) /\ ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) ) -> ( A e. V /\ B e. V /\ C e. V ) )
29 3simpb 
 |-  ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( A =/= B /\ B =/= C ) )
30 29 ad3antlr 
 |-  ( ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. 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 } C_ ( ( iEdg ` G ) ` i ) )
32 eqimss2 
 |-  ( ( ( iEdg ` G ) ` j ) = { B , C } -> { B , C } C_ ( ( iEdg ` G ) ` j ) )
33 31 32 anim12i 
 |-  ( ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) -> ( { A , B } C_ ( ( iEdg ` G ) ` i ) /\ { B , C } C_ ( ( iEdg ` G ) ` j ) ) )
34 33 adantl 
 |-  ( ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) /\ ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) ) -> ( { A , B } C_ ( ( iEdg ` G ) ` i ) /\ { B , C } 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 e. V /\ B e. V /\ C e. V ) -> ( A e. V /\ B e. V ) )
39 3simpc 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( B e. V /\ C e. V ) )
40 preq12bg 
 |-  ( ( ( A e. V /\ B e. V ) /\ ( B e. V /\ C e. V ) ) -> ( { A , B } = { B , C } <-> ( ( A = B /\ B = C ) \/ ( A = C /\ B = B ) ) ) )
41 38 39 40 syl2anc 
 |-  ( ( A e. V /\ B e. V /\ C e. 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 e. V /\ B e. V /\ C e. V ) -> ( { A , B } = { B , C } -> ( ( A =/= B /\ A =/= C /\ B =/= C ) -> i =/= j ) ) )
54 53 com23 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B } = { B , C } -> i =/= j ) ) )
55 54 adantl 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A =/= B /\ A =/= C /\ B =/= C ) -> ( { A , B } = { B , C } -> i =/= j ) ) )
56 55 imp 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( { A , B } = { B , C } -> i =/= j ) )
57 56 com12 
 |-  ( { A , B } = { B , C } -> ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> i =/= j ) )
58 37 57 syl 
 |-  ( ( ( ( iEdg ` G ) ` j ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) -> ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. 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 e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> i =/= j ) ) )
60 59 com23 
 |-  ( i = j -> ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) -> i =/= j ) ) )
61 2a1 
 |-  ( i =/= j -> ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. 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 e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) -> i =/= j ) )
63 62 adantr 
 |-  ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) -> ( ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) -> i =/= j ) )
64 63 imp 
 |-  ( ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) /\ ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) ) -> i =/= j )
65 simplr2 
 |-  ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) -> A =/= C )
66 65 adantr 
 |-  ( ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. 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 e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) /\ ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) ) -> <" i j "> ( A ( SPathsOn ` G ) C ) <" A B C "> )
68 s2len 
 |-  ( # ` <" i j "> ) = 2
69 67 68 jctir 
 |-  ( ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) /\ ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) ) -> ( <" i j "> ( A ( SPathsOn ` G ) C ) <" A B C "> /\ ( # ` <" i j "> ) = 2 ) )
70 breq12 
 |-  ( ( f = <" i j "> /\ p = <" A B C "> ) -> ( f ( A ( SPathsOn ` G ) C ) p <-> <" i j "> ( A ( SPathsOn ` G ) C ) <" A B C "> ) )
71 fveqeq2 
 |-  ( f = <" i j "> -> ( ( # ` f ) = 2 <-> ( # ` <" i j "> ) = 2 ) )
72 71 adantr 
 |-  ( ( f = <" i j "> /\ p = <" A B C "> ) -> ( ( # ` f ) = 2 <-> ( # ` <" i j "> ) = 2 ) )
73 70 72 anbi12d 
 |-  ( ( f = <" i j "> /\ p = <" A B C "> ) -> ( ( f ( A ( SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) <-> ( <" i j "> ( A ( SPathsOn ` G ) C ) <" A B C "> /\ ( # ` <" i j "> ) = 2 ) ) )
74 73 spc2egv 
 |-  ( ( <" i j "> e. _V /\ <" A B C "> e. _V ) -> ( ( <" i j "> ( A ( SPathsOn ` G ) C ) <" A B C "> /\ ( # ` <" i j "> ) = 2 ) -> E. f E. p ( f ( A ( SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) ) )
75 25 69 74 mpsyl 
 |-  ( ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) /\ ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) ) -> E. f E. p ( f ( A ( SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) )
76 75 ex 
 |-  ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) /\ ( i e. dom ( iEdg ` G ) /\ j e. dom ( iEdg ` G ) ) ) -> ( ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) -> E. f E. p ( f ( A ( SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) ) )
77 76 rexlimdvva 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( E. i e. dom ( iEdg ` G ) E. j e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` i ) = { A , B } /\ ( ( iEdg ` G ) ` j ) = { B , C } ) -> E. f E. p ( f ( A ( SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) ) )
78 20 77 sylbid 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) ) -> ( ( { A , B } e. E /\ { B , C } e. E ) -> E. f E. p ( f ( A ( SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) ) )
79 78 3impia 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( A =/= B /\ A =/= C /\ B =/= C ) /\ ( { A , B } e. E /\ { B , C } e. E ) ) -> E. f E. p ( f ( A ( SPathsOn ` G ) C ) p /\ ( # ` f ) = 2 ) )