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ℋ ) → ( Sℋ ⊆ Sℋ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ) )
7		neeq1	⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( Sℋ ≠ ∅ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) )
8	6 7	anbi12d	⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( ( Sℋ ⊆ Sℋ ∧ Sℋ ≠ ∅ ) ↔ ( if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ∧ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) ) )
9		ssid	⊢ Sℋ ⊆ Sℋ
10		h0elsh	⊢ 0ℋ ∈ Sℋ
11	10	ne0ii	⊢ Sℋ ≠ ∅
12	9 11	pm3.2i	⊢ ( Sℋ ⊆ Sℋ ∧ Sℋ ≠ ∅ )
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ℋ )