This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chintcli

Description: The intersection of a nonempty set of closed subspaces is a closed subspace. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis chintcl.1 
|- ( A C_ CH /\ A =/= (/) )
Assertion chintcli 
|- |^| A e. CH

Proof

Step Hyp Ref Expression
1 chintcl.1 
 |-  ( A C_ CH /\ A =/= (/) )
2 1 simpli 
 |-  A C_ CH
3 chsssh 
 |-  CH C_ SH
4 2 3 sstri 
 |-  A C_ SH
5 1 simpri 
 |-  A =/= (/)
6 4 5 pm3.2i 
 |-  ( A C_ SH /\ A =/= (/) )
7 6 shintcli 
 |-  |^| A e. SH
8 2 sseli 
 |-  ( y e. A -> y e. CH )
9 vex 
 |-  x e. _V
10 9 chlimi 
 |-  ( ( y e. CH /\ f : NN --> y /\ f ~~>v x ) -> x e. y )
11 10 3exp 
 |-  ( y e. CH -> ( f : NN --> y -> ( f ~~>v x -> x e. y ) ) )
12 11 com3r 
 |-  ( f ~~>v x -> ( y e. CH -> ( f : NN --> y -> x e. y ) ) )
13 8 12 syl5 
 |-  ( f ~~>v x -> ( y e. A -> ( f : NN --> y -> x e. y ) ) )
14 13 imp 
 |-  ( ( f ~~>v x /\ y e. A ) -> ( f : NN --> y -> x e. y ) )
15 14 ralimdva 
 |-  ( f ~~>v x -> ( A. y e. A f : NN --> y -> A. y e. A x e. y ) )
16 5 fint 
 |-  ( f : NN --> |^| A <-> A. y e. A f : NN --> y )
17 9 elint2 
 |-  ( x e. |^| A <-> A. y e. A x e. y )
18 15 16 17 3imtr4g 
 |-  ( f ~~>v x -> ( f : NN --> |^| A -> x e. |^| A ) )
19 18 impcom 
 |-  ( ( f : NN --> |^| A /\ f ~~>v x ) -> x e. |^| A )
20 19 gen2 
 |-  A. f A. x ( ( f : NN --> |^| A /\ f ~~>v x ) -> x e. |^| A )
21 isch2 
 |-  ( |^| A e. CH <-> ( |^| A e. SH /\ A. f A. x ( ( f : NN --> |^| A /\ f ~~>v x ) -> x e. |^| A ) ) )
22 7 20 21 mpbir2an 
 |-  |^| A e. CH