Metamath Proof Explorer

Theorem shintcl

Description: The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shintcl 
|- ( ( A C_ SH /\ A =/= (/) ) -> |^| A e. SH )

Proof

Step Hyp Ref Expression
1 inteq 
 |-  ( A = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> |^| A = |^| if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) )
2 1 eleq1d 
 |-  ( A = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> ( |^| A e. SH <-> |^| if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) e. SH ) )
3 sseq1 
 |-  ( A = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> ( A C_ SH <-> if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) C_ SH ) )
4 neeq1 
 |-  ( A = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> ( A =/= (/) <-> if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) =/= (/) ) )
5 3 4 anbi12d 
 |-  ( A = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> ( ( A C_ SH /\ A =/= (/) ) <-> ( if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) C_ SH /\ if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) =/= (/) ) ) )
6 sseq1 
 |-  ( SH = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> ( SH C_ SH <-> if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) C_ SH ) )
7 neeq1 
 |-  ( SH = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> ( SH =/= (/) <-> if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) =/= (/) ) )
8 6 7 anbi12d 
 |-  ( SH = if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) -> ( ( SH C_ SH /\ SH =/= (/) ) <-> ( if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) C_ SH /\ if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) =/= (/) ) ) )
9 ssid 
 |-  SH C_ SH
10 h0elsh 
 |-  0H e. SH
11 10 ne0ii 
 |-  SH =/= (/)
12 9 11 pm3.2i 
 |-  ( SH C_ SH /\ SH =/= (/) )
13 5 8 12 elimhyp 
 |-  ( if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) C_ SH /\ if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) =/= (/) )
14 13 shintcli 
 |-  |^| if ( ( A C_ SH /\ A =/= (/) ) , A , SH ) e. SH
15 2 14 dedth 
 |-  ( ( A C_ SH /\ A =/= (/) ) -> |^| A e. SH )