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

Metamath Proof Explorer

Theorem chintcl

Description: The intersection (infimum) of a nonempty subset of CH belongs to CH . Part of Theorem 3.13 of Beran p. 108. Also part of Definition 3.4-1 in MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion chintcl ⊢ A ⊆ C ℋ ∧ A ≠ ∅ → ⋂ A ∈ C ℋ

Proof

Step Hyp Ref Expression
1 inteq ⊢ A = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → ⋂ A = ⋂ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ
2 1 eleq1d ⊢ A = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → ⋂ A ∈ C ℋ ↔ ⋂ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ∈ C ℋ
3 sseq1 ⊢ A = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → A ⊆ C ℋ ↔ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ⊆ C ℋ
4 neeq1 ⊢ A = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → A ≠ ∅ ↔ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ≠ ∅
5 3 4 anbi12d ⊢ A = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → A ⊆ C ℋ ∧ A ≠ ∅ ↔ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ⊆ C ℋ ∧ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ≠ ∅
6 sseq1 ⊢ C ℋ = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → C ℋ ⊆ C ℋ ↔ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ⊆ C ℋ
7 neeq1 ⊢ C ℋ = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → C ℋ ≠ ∅ ↔ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ≠ ∅
8 6 7 anbi12d ⊢ C ℋ = if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ → C ℋ ⊆ C ℋ ∧ C ℋ ≠ ∅ ↔ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ⊆ C ℋ ∧ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ≠ ∅
9 ssid ⊢ C ℋ ⊆ C ℋ
10 h0elch ⊢ 0 ℋ ∈ C ℋ
11 10 ne0ii ⊢ C ℋ ≠ ∅
12 9 11 pm3.2i ⊢ C ℋ ⊆ C ℋ ∧ C ℋ ≠ ∅
13 5 8 12 elimhyp ⊢ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ⊆ C ℋ ∧ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ≠ ∅
14 13 chintcli ⊢ ⋂ if A ⊆ C ℋ ∧ A ≠ ∅ A C ℋ ∈ C ℋ
15 2 14 dedth ⊢ A ⊆ C ℋ ∧ A ≠ ∅ → ⋂ A ∈ C ℋ