Theorem frgrancvvdeqlem1 25814

Description: Lemma 1 for frgrancvvdeq 25826. (Contributed by Alexander van der Vekens, 22-Dec-2017.)

Hypotheses

Ref	Expression
frgrancvvdeq.nx	|- D = ( <. V , E >. Neighbors X )
frgrancvvdeq.ny	|- N = ( <. V , E >. Neighbors Y )
frgrancvvdeq.x	|- ( ph -> X e. V )
frgrancvvdeq.y	|- ( ph -> Y e. V )
frgrancvvdeq.ne	|- ( ph -> X =/= Y )
frgrancvvdeq.xy	|- ( ph -> Y e/ D )
frgrancvvdeq.f	|- ( ph -> V FriendGrph E )
frgrancvvdeq.a	|- A = ( x e. D |-> ( iota_ y e. N { x , y } e. ran E ) )

Assertion

Ref	Expression
frgrancvvdeqlem1	|- ( ( ph /\ x e. D ) -> Y e. ( V \ { x } ) )

Distinct variable groups:   y, D   x, y, V   x, E, y   y, Y   ph, y

Allowed substitution hints:   ph( x)   A( x, y)   D( x)   N( x, y)   X( x, y)   Y( x)

Proof of Theorem frgrancvvdeqlem1

Step	Hyp	Ref	Expression
1		frgrancvvdeq.y	. . 3 |- ( ph -> Y e. V )
2	1	adantr 471	. 2 |- ( ( ph /\ x e. D ) -> Y e. V )
3		frgrancvvdeq.xy	. . . . 5 |- ( ph -> Y e/ D )
4		df-nel 2636	. . . . . 6 |- ( Y e/ D <-> -. Y e. D )
5		eleq1a 2535	. . . . . . 7 |- ( x e. D -> ( Y = x -> Y e. D ) )
6	5	con3rr3 143	. . . . . 6 |- ( -. Y e. D -> ( x e. D -> -. Y = x ) )
7	4, 6	sylbi 200	. . . . 5 |- ( Y e/ D -> ( x e. D -> -. Y = x ) )
8	3, 7	syl 17	. . . 4 |- ( ph -> ( x e. D -> -. Y = x ) )
9	8	imp 435	. . 3 |- ( ( ph /\ x e. D ) -> -. Y = x )
10		elsncg 4003	. . . . 5 |- ( Y e. V -> ( Y e. { x } <-> Y = x ) )
11	1, 10	syl 17	. . . 4 |- ( ph -> ( Y e. { x } <-> Y = x ) )
12	11	adantr 471	. . 3 |- ( ( ph /\ x e. D ) -> ( Y e. { x } <-> Y = x ) )
13	9, 12	mtbird 307	. 2 |- ( ( ph /\ x e. D ) -> -. Y e. { x } )
14	2, 13	eldifd 3427	1 |- ( ( ph /\ x e. D ) -> Y e. ( V \ { x } ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   =/= wne 2633   e/ wnel 2634   \ cdif 3413   {csn 3980   {cpr 3982   <.cop 3986   class class class wbr 4418   |-> cmpt 4477   ran crn 4857   iota_crio 6281  (class class class)co 6320   Neighbors cnbgra 25201   FriendGrph cfrgra 25772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-nel 2636  df-v 3059  df-dif 3419  df-sn 3981

This theorem is referenced by:  frgrancvvdeqlem3  25816  frgrancvvdeqlem4  25817