MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nbgraf1olem1 Structured version   Unicode version

Theorem nbgraf1olem1 23369
Description: Lemma 1 for nbgraf1o 23375. For each neighbor of a vertex there is exactly one index for the edge between the vertex and its neighbor. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
Hypotheses
Ref Expression
nbgraf1o.n  |-  N  =  ( <. V ,  E >. Neighbors  U )
nbgraf1o.i  |-  I  =  { i  e.  dom  E  |  U  e.  ( E `  i ) }
nbgraf1o.f  |-  F  =  ( n  e.  N  |->  ( iota_ i  e.  I 
( E `  i
)  =  { U ,  n } ) )
Assertion
Ref Expression
nbgraf1olem1  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  M  e.  N
)  ->  E! i  e.  I  ( E `  i )  =  { U ,  M }
)
Distinct variable groups:    i, E, n    U, i, n    i, V, n    i, I, n   
n, N    i, M
Allowed substitution hints:    F( i, n)    M( n)    N( i)

Proof of Theorem nbgraf1olem1
Dummy variables  j  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nbgraf1o.n . . . . . 6  |-  N  =  ( <. V ,  E >. Neighbors  U )
21eleq2i 2507 . . . . 5  |-  ( M  e.  N  <->  M  e.  ( <. V ,  E >. Neighbors  U ) )
3 usgrav 23289 . . . . . . 7  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
43adantr 465 . . . . . 6  |-  ( ( V USGrph  E  /\  U  e.  V )  ->  ( V  e.  _V  /\  E  e.  _V ) )
5 nbgrael 23356 . . . . . 6  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( M  e.  (
<. V ,  E >. Neighbors  U
)  <->  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) ) )
64, 5syl 16 . . . . 5  |-  ( ( V USGrph  E  /\  U  e.  V )  ->  ( M  e.  ( <. V ,  E >. Neighbors  U )  <-> 
( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) ) )
72, 6syl5bb 257 . . . 4  |-  ( ( V USGrph  E  /\  U  e.  V )  ->  ( M  e.  N  <->  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) ) )
8 usgrafun 23296 . . . . . . . . . . . . . . . 16  |-  ( V USGrph  E  ->  Fun  E )
9 elrnrexdm 5866 . . . . . . . . . . . . . . . 16  |-  ( Fun 
E  ->  ( { U ,  M }  e.  ran  E  ->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) ) )
108, 9syl 16 . . . . . . . . . . . . . . 15  |-  ( V USGrph  E  ->  ( { U ,  M }  e.  ran  E  ->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) ) )
1110com12 31 . . . . . . . . . . . . . 14  |-  ( { U ,  M }  e.  ran  E  ->  ( V USGrph  E  ->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) ) )
12113ad2ant3 1011 . . . . . . . . . . . . 13  |-  ( ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E )  -> 
( V USGrph  E  ->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) ) )
1312com12 31 . . . . . . . . . . . 12  |-  ( V USGrph  E  ->  ( ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E )  ->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) ) )
1413adantr 465 . . . . . . . . . . 11  |-  ( ( V USGrph  E  /\  U  e.  V )  ->  (
( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E )  ->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) ) )
1514imp 429 . . . . . . . . . 10  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) )
16 eqcom 2445 . . . . . . . . . . 11  |-  ( ( E `  i )  =  { U ,  M }  <->  { U ,  M }  =  ( E `  i ) )
1716rexbii 2759 . . . . . . . . . 10  |-  ( E. i  e.  dom  E
( E `  i
)  =  { U ,  M }  <->  E. i  e.  dom  E { U ,  M }  =  ( E `  i ) )
1815, 17sylibr 212 . . . . . . . . 9  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  E. i  e.  dom  E ( E `
 i )  =  { U ,  M } )
19 prid1g 4000 . . . . . . . . . . . . . 14  |-  ( U  e.  V  ->  U  e.  { U ,  M } )
20 eleq2 2504 . . . . . . . . . . . . . 14  |-  ( ( E `  i )  =  { U ,  M }  ->  ( U  e.  ( E `  i )  <->  U  e.  { U ,  M }
) )
2119, 20syl5ibrcom 222 . . . . . . . . . . . . 13  |-  ( U  e.  V  ->  (
( E `  i
)  =  { U ,  M }  ->  U  e.  ( E `  i
) ) )
2221pm4.71rd 635 . . . . . . . . . . . 12  |-  ( U  e.  V  ->  (
( E `  i
)  =  { U ,  M }  <->  ( U  e.  ( E `  i
)  /\  ( E `  i )  =  { U ,  M }
) ) )
2322bicomd 201 . . . . . . . . . . 11  |-  ( U  e.  V  ->  (
( U  e.  ( E `  i )  /\  ( E `  i )  =  { U ,  M }
)  <->  ( E `  i )  =  { U ,  M }
) )
2423rexbidv 2755 . . . . . . . . . 10  |-  ( U  e.  V  ->  ( E. i  e.  dom  E ( U  e.  ( E `  i )  /\  ( E `  i )  =  { U ,  M }
)  <->  E. i  e.  dom  E ( E `  i
)  =  { U ,  M } ) )
2524ad2antlr 726 . . . . . . . . 9  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  ( E. i  e.  dom  E ( U  e.  ( E `
 i )  /\  ( E `  i )  =  { U ,  M } )  <->  E. i  e.  dom  E ( E `
 i )  =  { U ,  M } ) )
2618, 25mpbird 232 . . . . . . . 8  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  E. i  e.  dom  E ( U  e.  ( E `  i )  /\  ( E `  i )  =  { U ,  M } ) )
27 fveq2 5710 . . . . . . . . . 10  |-  ( x  =  i  ->  ( E `  x )  =  ( E `  i ) )
2827eleq2d 2510 . . . . . . . . 9  |-  ( x  =  i  ->  ( U  e.  ( E `  x )  <->  U  e.  ( E `  i ) ) )
2928rexrab 3142 . . . . . . . 8  |-  ( E. i  e.  { x  e.  dom  E  |  U  e.  ( E `  x
) }  ( E `
 i )  =  { U ,  M } 
<->  E. i  e.  dom  E ( U  e.  ( E `  i )  /\  ( E `  i )  =  { U ,  M }
) )
3026, 29sylibr 212 . . . . . . 7  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  E. i  e.  { x  e.  dom  E  |  U  e.  ( E `  x ) }  ( E `  i )  =  { U ,  M }
)
31 nbgraf1o.i . . . . . . . . 9  |-  I  =  { i  e.  dom  E  |  U  e.  ( E `  i ) }
32 fveq2 5710 . . . . . . . . . . 11  |-  ( i  =  x  ->  ( E `  i )  =  ( E `  x ) )
3332eleq2d 2510 . . . . . . . . . 10  |-  ( i  =  x  ->  ( U  e.  ( E `  i )  <->  U  e.  ( E `  x ) ) )
3433cbvrabv 2990 . . . . . . . . 9  |-  { i  e.  dom  E  |  U  e.  ( E `  i ) }  =  { x  e.  dom  E  |  U  e.  ( E `  x ) }
3531, 34eqtri 2463 . . . . . . . 8  |-  I  =  { x  e.  dom  E  |  U  e.  ( E `  x ) }
3635rexeqi 2941 . . . . . . 7  |-  ( E. i  e.  I  ( E `  i )  =  { U ,  M }  <->  E. i  e.  {
x  e.  dom  E  |  U  e.  ( E `  x ) }  ( E `  i )  =  { U ,  M }
)
3730, 36sylibr 212 . . . . . 6  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  E. i  e.  I  ( E `  i )  =  { U ,  M }
)
38 usgraf1o 23300 . . . . . . . . 9  |-  ( V USGrph  E  ->  E : dom  E -1-1-onto-> ran 
E )
39 dff1o6 6001 . . . . . . . . . 10  |-  ( E : dom  E -1-1-onto-> ran  E  <->  ( E  Fn  dom  E  /\  ran  E  =  ran  E  /\  A. i  e. 
dom  E A. j  e.  dom  E ( ( E `  i )  =  ( E `  j )  ->  i  =  j ) ) )
40 ssrab2 3456 . . . . . . . . . . . . . 14  |-  { i  e.  dom  E  |  U  e.  ( E `  i ) }  C_  dom  E
4131, 40eqsstri 3405 . . . . . . . . . . . . 13  |-  I  C_  dom  E
42 ssralv 3435 . . . . . . . . . . . . 13  |-  ( I 
C_  dom  E  ->  ( A. i  e.  dom  E A. j  e.  dom  E ( ( E `  i )  =  ( E `  j )  ->  i  =  j )  ->  A. i  e.  I  A. j  e.  dom  E ( ( E `  i )  =  ( E `  j )  ->  i  =  j ) ) )
4341, 42ax-mp 5 . . . . . . . . . . . 12  |-  ( A. i  e.  dom  E A. j  e.  dom  E ( ( E `  i
)  =  ( E `
 j )  -> 
i  =  j )  ->  A. i  e.  I  A. j  e.  dom  E ( ( E `  i )  =  ( E `  j )  ->  i  =  j ) )
44 ssralv 3435 . . . . . . . . . . . . . 14  |-  ( I 
C_  dom  E  ->  ( A. j  e.  dom  E ( ( E `  i )  =  ( E `  j )  ->  i  =  j )  ->  A. j  e.  I  ( ( E `  i )  =  ( E `  j )  ->  i  =  j ) ) )
4541, 44ax-mp 5 . . . . . . . . . . . . 13  |-  ( A. j  e.  dom  E ( ( E `  i
)  =  ( E `
 j )  -> 
i  =  j )  ->  A. j  e.  I 
( ( E `  i )  =  ( E `  j )  ->  i  =  j ) )
4645ralimi 2810 . . . . . . . . . . . 12  |-  ( A. i  e.  I  A. j  e.  dom  E ( ( E `  i
)  =  ( E `
 j )  -> 
i  =  j )  ->  A. i  e.  I  A. j  e.  I 
( ( E `  i )  =  ( E `  j )  ->  i  =  j ) )
47 eqtr3 2462 . . . . . . . . . . . . . . 15  |-  ( ( ( E `  i
)  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M } )  ->  ( E `  i )  =  ( E `  j ) )
4847imim1i 58 . . . . . . . . . . . . . 14  |-  ( ( ( E `  i
)  =  ( E `
 j )  -> 
i  =  j )  ->  ( ( ( E `  i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M } )  ->  i  =  j ) )
4948ralimi 2810 . . . . . . . . . . . . 13  |-  ( A. j  e.  I  (
( E `  i
)  =  ( E `
 j )  -> 
i  =  j )  ->  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) )
5049ralimi 2810 . . . . . . . . . . . 12  |-  ( A. i  e.  I  A. j  e.  I  (
( E `  i
)  =  ( E `
 j )  -> 
i  =  j )  ->  A. i  e.  I  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) )
5143, 46, 503syl 20 . . . . . . . . . . 11  |-  ( A. i  e.  dom  E A. j  e.  dom  E ( ( E `  i
)  =  ( E `
 j )  -> 
i  =  j )  ->  A. i  e.  I  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) )
52513ad2ant3 1011 . . . . . . . . . 10  |-  ( ( E  Fn  dom  E  /\  ran  E  =  ran  E  /\  A. i  e. 
dom  E A. j  e.  dom  E ( ( E `  i )  =  ( E `  j )  ->  i  =  j ) )  ->  A. i  e.  I  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) )
5339, 52sylbi 195 . . . . . . . . 9  |-  ( E : dom  E -1-1-onto-> ran  E  ->  A. i  e.  I  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) )
5438, 53syl 16 . . . . . . . 8  |-  ( V USGrph  E  ->  A. i  e.  I  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) )
5554adantr 465 . . . . . . 7  |-  ( ( V USGrph  E  /\  U  e.  V )  ->  A. i  e.  I  A. j  e.  I  ( (
( E `  i
)  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M } )  ->  i  =  j ) )
5655adantr 465 . . . . . 6  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  A. i  e.  I  A. j  e.  I  ( (
( E `  i
)  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M } )  ->  i  =  j ) )
5737, 56jca 532 . . . . 5  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  ( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E ) )  ->  ( E. i  e.  I  ( E `  i )  =  { U ,  M }  /\  A. i  e.  I  A. j  e.  I  ( ( ( E `  i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M } )  ->  i  =  j ) ) )
5857ex 434 . . . 4  |-  ( ( V USGrph  E  /\  U  e.  V )  ->  (
( U  e.  V  /\  M  e.  V  /\  { U ,  M }  e.  ran  E )  ->  ( E. i  e.  I  ( E `  i )  =  { U ,  M }  /\  A. i  e.  I  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) ) ) )
597, 58sylbid 215 . . 3  |-  ( ( V USGrph  E  /\  U  e.  V )  ->  ( M  e.  N  ->  ( E. i  e.  I 
( E `  i
)  =  { U ,  M }  /\  A. i  e.  I  A. j  e.  I  (
( ( E `  i )  =  { U ,  M }  /\  ( E `  j
)  =  { U ,  M } )  -> 
i  =  j ) ) ) )
6059imp 429 . 2  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  M  e.  N
)  ->  ( E. i  e.  I  ( E `  i )  =  { U ,  M }  /\  A. i  e.  I  A. j  e.  I  ( ( ( E `  i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M } )  ->  i  =  j ) ) )
61 fveq2 5710 . . . 4  |-  ( i  =  j  ->  ( E `  i )  =  ( E `  j ) )
6261eqeq1d 2451 . . 3  |-  ( i  =  j  ->  (
( E `  i
)  =  { U ,  M }  <->  ( E `  j )  =  { U ,  M }
) )
6362reu4 3172 . 2  |-  ( E! i  e.  I  ( E `  i )  =  { U ,  M }  <->  ( E. i  e.  I  ( E `  i )  =  { U ,  M }  /\  A. i  e.  I  A. j  e.  I 
( ( ( E `
 i )  =  { U ,  M }  /\  ( E `  j )  =  { U ,  M }
)  ->  i  =  j ) ) )
6460, 63sylibr 212 1  |-  ( ( ( V USGrph  E  /\  U  e.  V )  /\  M  e.  N
)  ->  E! i  e.  I  ( E `  i )  =  { U ,  M }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   A.wral 2734   E.wrex 2735   E!wreu 2736   {crab 2738   _Vcvv 2991    C_ wss 3347   {cpr 3898   <.cop 3902   class class class wbr 4311    e. cmpt 4369   dom cdm 4859   ran crn 4860   Fun wfun 5431    Fn wfn 5432   -1-1-onto->wf1o 5436   ` cfv 5437   iota_crio 6070  (class class class)co 6110   USGrph cusg 23283   Neighbors cnbgra 23348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550  ax-un 6391  ax-cnex 9357  ax-resscn 9358  ax-1cn 9359  ax-icn 9360  ax-addcl 9361  ax-addrcl 9362  ax-mulcl 9363  ax-mulrcl 9364  ax-mulcom 9365  ax-addass 9366  ax-mulass 9367  ax-distr 9368  ax-i2m1 9369  ax-1ne0 9370  ax-1rid 9371  ax-rnegex 9372  ax-rrecex 9373  ax-cnre 9374  ax-pre-lttri 9375  ax-pre-lttrn 9376  ax-pre-ltadd 9377  ax-pre-mulgt0 9378
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2739  df-rex 2740  df-reu 2741  df-rmo 2742  df-rab 2743  df-v 2993  df-sbc 3206  df-csb 3308  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-pss 3363  df-nul 3657  df-if 3811  df-pw 3881  df-sn 3897  df-pr 3899  df-tp 3901  df-op 3903  df-uni 4111  df-int 4148  df-iun 4192  df-br 4312  df-opab 4370  df-mpt 4371  df-tr 4405  df-eprel 4651  df-id 4655  df-po 4660  df-so 4661  df-fr 4698  df-we 4700  df-ord 4741  df-on 4742  df-lim 4743  df-suc 4744  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5400  df-fun 5439  df-fn 5440  df-f 5441  df-f1 5442  df-fo 5443  df-f1o 5444  df-fv 5445  df-riota 6071  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-om 6496  df-1st 6596  df-2nd 6597  df-recs 6851  df-rdg 6885  df-1o 6939  df-er 7120  df-en 7330  df-dom 7331  df-sdom 7332  df-fin 7333  df-card 8128  df-pnf 9439  df-mnf 9440  df-xr 9441  df-ltxr 9442  df-le 9443  df-sub 9616  df-neg 9617  df-nn 10342  df-2 10399  df-n0 10599  df-z 10666  df-uz 10881  df-fz 11457  df-hash 12123  df-usgra 23285  df-nbgra 23351
This theorem is referenced by:  nbgraf1olem2  23370  nbgraf1olem3  23371
  Copyright terms: Public domain W3C validator