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