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

Theorem nbgraopALT 24642
Description: Alternate proof of nbgraop 24641 using mpt2xopoveq 6965, but being longer. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
nbgraopALT  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( <. V ,  E >. Neighbors  N
)  =  { n  e.  V  |  { N ,  n }  e.  ran  E } )
Distinct variable groups:    n, V    n, E    n, N    n, Y    n, Z

Proof of Theorem nbgraopALT
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nbgra 24638 . . 3  |- Neighbors  =  ( x  e.  _V , 
y  e.  ( 1st `  x )  |->  { n  e.  ( 1st `  x
)  |  { y ,  n }  e.  ran  ( 2nd `  x
) } )
21mpt2xopoveq 6965 . 2  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( <. V ,  E >. Neighbors  N
)  =  { n  e.  V  |  [. <. V ,  E >.  /  x ]. [. N  /  y ]. { y ,  n }  e.  ran  ( 2nd `  x ) } )
3 sbcel1g 3837 . . . . . 6  |-  ( N  e.  V  ->  ( [. N  /  y ]. { y ,  n }  e.  ran  ( 2nd `  x )  <->  [_ N  / 
y ]_ { y ,  n }  e.  ran  ( 2nd `  x ) ) )
43adantl 466 . . . . 5  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( [. N  /  y ]. { y ,  n }  e.  ran  ( 2nd `  x )  <->  [_ N  / 
y ]_ { y ,  n }  e.  ran  ( 2nd `  x ) ) )
54sbcbidv 3386 . . . 4  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( [. <. V ,  E >.  /  x ]. [. N  /  y ]. {
y ,  n }  e.  ran  ( 2nd `  x
)  <->  [. <. V ,  E >.  /  x ]. [_ N  /  y ]_ {
y ,  n }  e.  ran  ( 2nd `  x
) ) )
6 sbcel2 3839 . . . . 5  |-  ( [. <. V ,  E >.  /  x ]. [_ N  /  y ]_ {
y ,  n }  e.  ran  ( 2nd `  x
)  <->  [_ N  /  y ]_ { y ,  n }  e.  [_ <. V ,  E >.  /  x ]_ ran  ( 2nd `  x
) )
76a1i 11 . . . 4  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( [. <. V ,  E >.  /  x ]. [_ N  /  y ]_ {
y ,  n }  e.  ran  ( 2nd `  x
)  <->  [_ N  /  y ]_ { y ,  n }  e.  [_ <. V ,  E >.  /  x ]_ ran  ( 2nd `  x
) ) )
8 df-pr 4035 . . . . . . . 8  |-  { y ,  n }  =  ( { y }  u.  { n } )
98a1i 11 . . . . . . 7  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  { y ,  n }  =  ( { y }  u.  { n } ) )
109csbeq2dv 3843 . . . . . 6  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ N  /  y ]_ {
y ,  n }  =  [_ N  /  y ]_ ( { y }  u.  { n }
) )
11 nfcv 2619 . . . . . . . . 9  |-  F/_ y
( { N }  u.  { n } )
1211a1i 11 . . . . . . . 8  |-  ( N  e.  V  ->  F/_ y
( { N }  u.  { n } ) )
13 sneq 4042 . . . . . . . . 9  |-  ( y  =  N  ->  { y }  =  { N } )
1413uneq1d 3653 . . . . . . . 8  |-  ( y  =  N  ->  ( { y }  u.  { n } )  =  ( { N }  u.  { n } ) )
1512, 14csbiegf 3454 . . . . . . 7  |-  ( N  e.  V  ->  [_ N  /  y ]_ ( { y }  u.  { n } )  =  ( { N }  u.  { n } ) )
1615adantl 466 . . . . . 6  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ N  /  y ]_ ( { y }  u.  { n } )  =  ( { N }  u.  { n } ) )
17 df-pr 4035 . . . . . . . 8  |-  { N ,  n }  =  ( { N }  u.  { n } )
1817eqcomi 2470 . . . . . . 7  |-  ( { N }  u.  {
n } )  =  { N ,  n }
1918a1i 11 . . . . . 6  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( { N }  u.  {
n } )  =  { N ,  n } )
2010, 16, 193eqtrd 2502 . . . . 5  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ N  /  y ]_ {
y ,  n }  =  { N ,  n } )
21 csbrn 5474 . . . . . . 7  |-  [_ <. V ,  E >.  /  x ]_ ran  ( 2nd `  x
)  =  ran  [_ <. V ,  E >.  /  x ]_ ( 2nd `  x
)
2221a1i 11 . . . . . 6  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ <. V ,  E >.  /  x ]_ ran  ( 2nd `  x
)  =  ran  [_ <. V ,  E >.  /  x ]_ ( 2nd `  x
) )
23 opex 4720 . . . . . . . . 9  |-  <. V ,  E >.  e.  _V
24 csbfv2g 5908 . . . . . . . . 9  |-  ( <. V ,  E >.  e. 
_V  ->  [_ <. V ,  E >.  /  x ]_ ( 2nd `  x )  =  ( 2nd `  [_ <. V ,  E >.  /  x ]_ x ) )
2523, 24mp1i 12 . . . . . . . 8  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ <. V ,  E >.  /  x ]_ ( 2nd `  x
)  =  ( 2nd `  [_ <. V ,  E >.  /  x ]_ x
) )
26 csbvarg 3855 . . . . . . . . . 10  |-  ( <. V ,  E >.  e. 
_V  ->  [_ <. V ,  E >.  /  x ]_ x  =  <. V ,  E >. )
2723, 26mp1i 12 . . . . . . . . 9  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ <. V ,  E >.  /  x ]_ x  =  <. V ,  E >. )
2827fveq2d 5876 . . . . . . . 8  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( 2nd `  [_ <. V ,  E >.  /  x ]_ x )  =  ( 2nd `  <. V ,  E >. ) )
29 op2ndg 6812 . . . . . . . . 9  |-  ( ( V  e.  Y  /\  E  e.  Z )  ->  ( 2nd `  <. V ,  E >. )  =  E )
3029adantr 465 . . . . . . . 8  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( 2nd `  <. V ,  E >. )  =  E )
3125, 28, 303eqtrd 2502 . . . . . . 7  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ <. V ,  E >.  /  x ]_ ( 2nd `  x
)  =  E )
3231rneqd 5240 . . . . . 6  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ran  [_
<. V ,  E >.  /  x ]_ ( 2nd `  x )  =  ran  E )
3322, 32eqtrd 2498 . . . . 5  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  [_ <. V ,  E >.  /  x ]_ ran  ( 2nd `  x
)  =  ran  E
)
3420, 33eleq12d 2539 . . . 4  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( [_ N  /  y ]_ { y ,  n }  e.  [_ <. V ,  E >.  /  x ]_ ran  ( 2nd `  x
)  <->  { N ,  n }  e.  ran  E ) )
355, 7, 343bitrd 279 . . 3  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( [. <. V ,  E >.  /  x ]. [. N  /  y ]. {
y ,  n }  e.  ran  ( 2nd `  x
)  <->  { N ,  n }  e.  ran  E ) )
3635rabbidv 3101 . 2  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  { n  e.  V  |  [. <. V ,  E >.  /  x ]. [. N  /  y ]. { y ,  n }  e.  ran  ( 2nd `  x ) }  =  { n  e.  V  |  { N ,  n }  e.  ran  E }
)
372, 36eqtrd 2498 1  |-  ( ( ( V  e.  Y  /\  E  e.  Z
)  /\  N  e.  V )  ->  ( <. V ,  E >. Neighbors  N
)  =  { n  e.  V  |  { N ,  n }  e.  ran  E } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1395    e. wcel 1819   F/_wnfc 2605   {crab 2811   _Vcvv 3109   [.wsbc 3327   [_csb 3430    u. cun 3469   {csn 4032   {cpr 4034   <.cop 4038   ran crn 5009   ` cfv 5594  (class class class)co 6296   2ndc2nd 6798   Neighbors cnbgra 24635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6799  df-2nd 6800  df-nbgra 24638
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator