Theorem neissex 16812

Description: For any neighborhood N of S, there is a neighborhood x of S such that N is a neighborhood of all subsets of x. Proposition Viv of [BourbakiTop1] p. I.3 . (Contributed by FL, 2-Oct-2006.)

Assertion

Ref	Expression
neissex	|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )

Distinct variable groups:   x, y, J   x, N, y   x, S, y

Proof of Theorem neissex

Step	Hyp	Ref	Expression
1		neii2 16793	. 2 |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. J ( S C_ x /\ x C_ N ) )
2		opnneiss 16803	. . . . . . . 8 |- ( ( J e. Top /\ x e. J /\ S C_ x ) -> x e. ( ( nei ` J ) ` S ) )
3	2	3expb 1157	. . . . . . 7 |- ( ( J e. Top /\ ( x e. J /\ S C_ x ) ) -> x e. ( ( nei ` J ) ` S ) )
4	3	adantrrr 708	. . . . . 6 |- ( ( J e. Top /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> x e. ( ( nei ` J ) ` S ) )
5	4	adantlr 698	. . . . 5 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> x e. ( ( nei ` J ) ` S ) )
6		simplll 737	. . . . . . . . 9 |- ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> J e. Top )
7		simpll 733	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> J e. Top )
8		simpr 449	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> x e. J )
9		eqid 2256	. . . . . . . . . . . . . . 15 |- U. J = U. J
10	9	neii1 16791	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ U. J )
11	10	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> N C_ U. J )
12	9	opnssneib 16800	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ x e. J /\ N C_ U. J ) -> ( x C_ N <-> N e. ( ( nei ` J ) ` x ) ) )
13	7, 8, 11, 12	syl3anc 1187	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) -> ( x C_ N <-> N e. ( ( nei ` J ) ` x ) ) )
14	13	biimpa 472	. . . . . . . . . . 11 |- ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ x e. J ) /\ x C_ N ) -> N e. ( ( nei ` J ) ` x ) )
15	14	anasss 631	. . . . . . . . . 10 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) -> N e. ( ( nei ` J ) ` x ) )
16	15	adantr 453	. . . . . . . . 9 |- ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> N e. ( ( nei ` J ) ` x ) )
17		simpr 449	. . . . . . . . 9 |- ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> y C_ x )
18		neiss 16794	. . . . . . . . 9 |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` x ) /\ y C_ x ) -> N e. ( ( nei ` J ) ` y ) )
19	6, 16, 17, 18	syl3anc 1187	. . . . . . . 8 |- ( ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) /\ y C_ x ) -> N e. ( ( nei ` J ) ` y ) )
20	19	ex 425	. . . . . . 7 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ x C_ N ) ) -> ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
21	20	adantrrl 707	. . . . . 6 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
22	21	alrimiv 2013	. . . . 5 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
23	5, 22	jca 520	. . . 4 |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( x e. J /\ ( S C_ x /\ x C_ N ) ) ) -> ( x e. ( ( nei ` J ) ` S ) /\ A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) ) )
24	23	ex 425	. . 3 |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( ( x e. J /\ ( S C_ x /\ x C_ N ) ) -> ( x e. ( ( nei ` J ) ` S ) /\ A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) ) ) )
25	24	reximdv2 2625	. 2 |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> ( E. x e. J ( S C_ x /\ x C_ N ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) ) )
26	1, 25	mpd 16	1 |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )

Syntax hints:   -> wi 6   <-> wb 178   /\ wa 360   A.wal 1532   e. wcel 1621   E.wrex 2517   C_ wss 3113   U.cuni 3787   ` cfv 4659   Topctop 16579   neicnei 16782

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4091  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-reu 2523  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-iun 3867  df-br 3984  df-opab 4038  df-mpt 4039  df-id 4267  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-top 16584  df-nei 16783