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 ( ( 𝐴S𝐴 ≠ ∅ ) → 𝐴S )

Proof

Step Hyp Ref Expression
1 inteq ( 𝐴 = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → 𝐴 = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) )
2 1 eleq1d ( 𝐴 = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → ( 𝐴S if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ∈ S ) )
3 sseq1 ( 𝐴 = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → ( 𝐴S ↔ if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ⊆ S ) )
4 neeq1 ( 𝐴 = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → ( 𝐴 ≠ ∅ ↔ if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ≠ ∅ ) )
5 3 4 anbi12d ( 𝐴 = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → ( ( 𝐴S𝐴 ≠ ∅ ) ↔ ( if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ⊆ S ∧ if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ≠ ∅ ) ) )
6 sseq1 ( S = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → ( SS ↔ if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ⊆ S ) )
7 neeq1 ( S = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → ( S ≠ ∅ ↔ if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ≠ ∅ ) )
8 6 7 anbi12d ( S = if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) → ( ( SSS ≠ ∅ ) ↔ ( if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ⊆ S ∧ if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ≠ ∅ ) ) )
9 ssid SS
10 h0elsh 0S
11 10 ne0ii S ≠ ∅
12 9 11 pm3.2i ( SSS ≠ ∅ )
13 5 8 12 elimhyp ( if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ⊆ S ∧ if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ≠ ∅ )
14 13 shintcli if ( ( 𝐴S𝐴 ≠ ∅ ) , 𝐴 , S ) ∈ S
15 2 14 dedth ( ( 𝐴S𝐴 ≠ ∅ ) → 𝐴S )