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

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 ⊆ S ℋ ∧ A ≠ ∅ → ⋂ A ∈ S ℋ

Proof

Step Hyp Ref Expression
1 inteq ⊢ A = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → ⋂ A = ⋂ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ
2 1 eleq1d ⊢ A = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → ⋂ A ∈ S ℋ ↔ ⋂ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ∈ S ℋ
3 sseq1 ⊢ A = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → A ⊆ S ℋ ↔ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ⊆ S ℋ
4 neeq1 ⊢ A = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → A ≠ ∅ ↔ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ≠ ∅
5 3 4 anbi12d ⊢ A = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → A ⊆ S ℋ ∧ A ≠ ∅ ↔ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ⊆ S ℋ ∧ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ≠ ∅
6 sseq1 ⊢ S ℋ = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → S ℋ ⊆ S ℋ ↔ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ⊆ S ℋ
7 neeq1 ⊢ S ℋ = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → S ℋ ≠ ∅ ↔ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ≠ ∅
8 6 7 anbi12d ⊢ S ℋ = if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ → S ℋ ⊆ S ℋ ∧ S ℋ ≠ ∅ ↔ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ⊆ S ℋ ∧ if A ⊆ S ℋ ∧ A ≠ ∅ A 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 A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ⊆ S ℋ ∧ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ≠ ∅
14 13 shintcli ⊢ ⋂ if A ⊆ S ℋ ∧ A ≠ ∅ A S ℋ ∈ S ℋ
15 2 14 dedth ⊢ A ⊆ S ℋ ∧ A ≠ ∅ → ⋂ A ∈ S ℋ