Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  neissex Unicode version

Theorem neissex 12116
 Description: For any neighborhood of , there is a neighborhood of such that is a neighborhood of all subsets of . Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
Assertion
Ref Expression
neissex
Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem neissex
StepHypRef Expression
1 neii2 12100 . 2
2 opnneiss 12109 . . . . 5
323expb 1150 . . . 4
6 simplll 503 . . . . . 6
7 simpll 499 . . . . . . . . . 10
8 simpr 109 . . . . . . . . . 10
9 eqid 2100 . . . . . . . . . . . 12
109neii1 12098 . . . . . . . . . . 11
1110adantr 272 . . . . . . . . . 10
129opnssneib 12107 . . . . . . . . . 10
137, 8, 11, 12syl3anc 1184 . . . . . . . . 9
1413biimpa 292 . . . . . . . 8
1514anasss 394 . . . . . . 7
1615adantr 272 . . . . . 6
17 simpr 109 . . . . . 6
18 neiss 12101 . . . . . 6
196, 16, 17, 18syl3anc 1184 . . . . 5
2019ex 114 . . . 4