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 e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p )

Proof

Step Hyp Ref Expression
1 1pthon2v.v 
 |-  V = ( Vtx ` G )
2 1pthon2v.e 
 |-  E = ( Edg ` G )
3 simpl 
 |-  ( ( A e. V /\ B e. V ) -> A e. V )
4 3 anim2i 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) ) -> ( G e. UHGraph /\ A e. V ) )
5 4 3adant3 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> ( G e. UHGraph /\ A e. V ) )
6 5 adantl 
 |-  ( ( A = B /\ ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) ) -> ( G e. UHGraph /\ A e. V ) )
7 1 0pthonv 
 |-  ( A e. V -> E. f E. p f ( A ( PathsOn ` G ) A ) p )
8 6 7 simpl2im 
 |-  ( ( A = B /\ ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) ) -> E. f E. p f ( A ( PathsOn ` G ) A ) p )
9 oveq2 
 |-  ( B = A -> ( A ( PathsOn ` G ) B ) = ( A ( PathsOn ` G ) A ) )
10 9 eqcoms 
 |-  ( A = B -> ( A ( PathsOn ` G ) B ) = ( A ( PathsOn ` G ) A ) )
11 10 breqd 
 |-  ( A = B -> ( f ( A ( PathsOn ` G ) B ) p <-> f ( A ( PathsOn ` G ) A ) p ) )
12 11 2exbidv 
 |-  ( A = B -> ( E. f E. p f ( A ( PathsOn ` G ) B ) p <-> E. f E. p f ( A ( PathsOn ` G ) A ) p ) )
13 12 adantr 
 |-  ( ( A = B /\ ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) ) -> ( E. f E. p f ( A ( PathsOn ` G ) B ) p <-> E. f E. p f ( A ( PathsOn ` G ) A ) p ) )
14 8 13 mpbird 
 |-  ( ( A = B /\ ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p )
15 14 ex 
 |-  ( A = B -> ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) )
16 2 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
17 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
18 17 uhgredgiedgb 
 |-  ( G e. UHGraph -> ( e e. ( Edg ` G ) <-> E. i e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` i ) ) )
19 16 18 bitrid 
 |-  ( G e. UHGraph -> ( e e. E <-> E. i e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` i ) ) )
20 19 3ad2ant1 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( e e. E <-> E. i e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` i ) ) )
21 s1cli 
 |-  <" i "> e. Word _V
22 s2cli 
 |-  <" A B "> e. Word _V
23 21 22 pm3.2i 
 |-  ( <" i "> e. Word _V /\ <" A B "> e. Word _V )
24 eqid 
 |-  <" A B "> = <" A B ">
25 eqid 
 |-  <" i "> = <" i ">
26 simpl2l 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) -> A e. V )
27 simpl2r 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) -> B e. 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 e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( A = B -> ( ( iEdg ` G ) ` i ) = { A } ) )
31 30 adantr 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) -> ( A = B -> ( ( iEdg ` G ) ` i ) = { A } ) )
32 31 imp 
 |-  ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) /\ A = B ) -> ( ( iEdg ` G ) ` i ) = { A } )
33 sseq2 
 |-  ( e = ( ( iEdg ` G ) ` i ) -> ( { A , B } C_ e <-> { A , B } C_ ( ( iEdg ` G ) ` i ) ) )
34 33 adantl 
 |-  ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) -> ( { A , B } C_ e <-> { A , B } C_ ( ( iEdg ` G ) ` i ) ) )
35 34 biimpa 
 |-  ( ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) -> { A , B } C_ ( ( iEdg ` G ) ` i ) )
36 35 adantl 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) -> { A , B } C_ ( ( iEdg ` G ) ` i ) )
37 36 adantr 
 |-  ( ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) /\ A =/= B ) -> { A , B } C_ ( ( iEdg ` G ) ` i ) )
38 24 25 26 27 32 37 1 17 1pthond 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) -> <" i "> ( A ( PathsOn ` G ) B ) <" A B "> )
39 breq12 
 |-  ( ( f = <" i "> /\ p = <" A B "> ) -> ( f ( A ( PathsOn ` G ) B ) p <-> <" i "> ( A ( PathsOn ` G ) B ) <" A B "> ) )
40 39 spc2egv 
 |-  ( ( <" i "> e. Word _V /\ <" A B "> e. Word _V ) -> ( <" i "> ( A ( PathsOn ` G ) B ) <" A B "> -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) )
41 23 38 40 mpsyl 
 |-  ( ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) /\ ( ( i e. dom ( iEdg ` G ) /\ e = ( ( iEdg ` G ) ` i ) ) /\ { A , B } C_ e ) ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p )
42 41 exp44 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( i e. dom ( iEdg ` G ) -> ( e = ( ( iEdg ` G ) ` i ) -> ( { A , B } C_ e -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) ) ) )
43 42 rexlimdv 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( E. i e. dom ( iEdg ` G ) e = ( ( iEdg ` G ) ` i ) -> ( { A , B } C_ e -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) ) )
44 20 43 sylbid 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( e e. E -> ( { A , B } C_ e -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) ) )
45 44 rexlimdv 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( E. e e. E { A , B } C_ e -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) )
46 45 3exp 
 |-  ( G e. UHGraph -> ( ( A e. V /\ B e. V ) -> ( A =/= B -> ( E. e e. E { A , B } C_ e -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) ) ) )
47 46 com34 
 |-  ( G e. UHGraph -> ( ( A e. V /\ B e. V ) -> ( E. e e. E { A , B } C_ e -> ( A =/= B -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) ) ) )
48 47 3imp 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> ( A =/= B -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) )
49 48 com12 
 |-  ( A =/= B -> ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p ) )
50 15 49 pm2.61ine 
 |-  ( ( G e. UHGraph /\ ( A e. V /\ B e. V ) /\ E. e e. E { A , B } C_ e ) -> E. f E. p f ( A ( PathsOn ` G ) B ) p )