Theorem nbgraopALT 25152

Description: Alternate proof of nbgraop 25151 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.

Step	Hyp	Ref	Expression
1		df-nbgra 25148	. . 3 |- Neighbors = ( x e. _V , y e. ( 1st ` x ) |-> { n e. ( 1st ` x ) | { y , n } e. ran ( 2nd ` x ) } )
2	1	mpt2xopoveq 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 3776	. . . . . 6 |- ( N e. V -> ( [. N / y ]. { y , n } e. ran ( 2nd ` x ) <-> [_ N / y ]_ { y , n } e. ran ( 2nd ` x ) ) )
4	3	adantl 468	. . . . 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 ) ) )
5	4	sbcbidv 3322	. . . 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 3778	. . . . 5 |- ( [. <. V , E >. / x ]. [_ N / y ]_ { y , n } e. ran ( 2nd ` x ) <-> [_ N / y ]_ { y , n } e. [_ <. V , E >. / x ]_ ran ( 2nd ` x ) )
7	6	a1i 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 3971	. . . . . . . 8 |- { y , n } = ( { y } u. { n } )
9	8	a1i 11	. . . . . . 7 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> { y , n } = ( { y } u. { n } ) )
10	9	csbeq2dv 3781	. . . . . 6 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> [_ N / y ]_ { y , n } = [_ N / y ]_ ( { y } u. { n } ) )
11		nfcv 2592	. . . . . . . . 9 |- F/_ y ( { N } u. { n } )
12	11	a1i 11	. . . . . . . 8 |- ( N e. V -> F/_ y ( { N } u. { n } ) )
13		sneq 3978	. . . . . . . . 9 |- ( y = N -> { y } = { N } )
14	13	uneq1d 3587	. . . . . . . 8 |- ( y = N -> ( { y } u. { n } ) = ( { N } u. { n } ) )
15	12, 14	csbiegf 3387	. . . . . . 7 |- ( N e. V -> [_ N / y ]_ ( { y } u. { n } ) = ( { N } u. { n } ) )
16	15	adantl 468	. . . . . 6 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> [_ N / y ]_ ( { y } u. { n } ) = ( { N } u. { n } ) )
17		df-pr 3971	. . . . . . . 8 |- { N , n } = ( { N } u. { n } )
18	17	eqcomi 2460	. . . . . . 7 |- ( { N } u. { n } ) = { N , n }
19	18	a1i 11	. . . . . 6 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> ( { N } u. { n } ) = { N , n } )
20	10, 16, 19	3eqtrd 2489	. . . . 5 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> [_ N / y ]_ { y , n } = { N , n } )
21		csbrn 5297	. . . . . . 7 |- [_ <. V , E >. / x ]_ ran ( 2nd ` x ) = ran [_ <. V , E >. / x ]_ ( 2nd ` x )
22	21	a1i 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 4664	. . . . . . . . 9 |- <. V , E >. e. _V
24		csbfv2g 5901	. . . . . . . . 9 |- ( <. V , E >. e. _V -> [_ <. V , E >. / x ]_ ( 2nd ` x ) = ( 2nd ` [_ <. V , E >. / x ]_ x ) )
25	23, 24	mp1i 13	. . . . . . . 8 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> [_ <. V , E >. / x ]_ ( 2nd ` x ) = ( 2nd ` [_ <. V , E >. / x ]_ x ) )
26		csbvarg 3792	. . . . . . . . . 10 |- ( <. V , E >. e. _V -> [_ <. V , E >. / x ]_ x = <. V , E >. )
27	23, 26	mp1i 13	. . . . . . . . 9 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> [_ <. V , E >. / x ]_ x = <. V , E >. )
28	27	fveq2d 5869	. . . . . . . 8 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> ( 2nd ` [_ <. V , E >. / x ]_ x ) = ( 2nd ` <. V , E >. ) )
29		op2ndg 6806	. . . . . . . . 9 |- ( ( V e. Y /\ E e. Z ) -> ( 2nd ` <. V , E >. ) = E )
30	29	adantr 467	. . . . . . . 8 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> ( 2nd ` <. V , E >. ) = E )
31	25, 28, 30	3eqtrd 2489	. . . . . . 7 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> [_ <. V , E >. / x ]_ ( 2nd ` x ) = E )
32	31	rneqd 5062	. . . . . 6 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> ran [_ <. V , E >. / x ]_ ( 2nd ` x ) = ran E )
33	22, 32	eqtrd 2485	. . . . 5 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> [_ <. V , E >. / x ]_ ran ( 2nd ` x ) = ran E )
34	20, 33	eleq12d 2523	. . . 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 ) )
35	5, 7, 34	3bitrd 283	. . 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 ) )
36	35	rabbidv 3036	. 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 } )
37	2, 36	eqtrd 2485	1 |- ( ( ( V e. Y /\ E e. Z ) /\ N e. V ) -> ( <. V , E >. Neighbors N ) = { n e. V | { N , n } e. ran E } )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1444   e. wcel 1887   F/_wnfc 2579   {crab 2741   _Vcvv 3045   [.wsbc 3267   [_csb 3363   u. cun 3402   {csn 3968   {cpr 3970   <.cop 3974   ran crn 4835   ` cfv 5582  (class class class)co 6290   2ndc2nd 6792   Neighbors cnbgra 25145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-nbgra 25148

This theorem is referenced by: (None)