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 ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Cℋ )

Proof

Step Hyp Ref Expression
1 inteq ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ∩ 𝐴 = ∩ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) )
2 1 eleq1d ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ( ∩ 𝐴 ∈ Cℋ ↔ ∩ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ∈ Cℋ ) )
3 sseq1 ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ( 𝐴 ⊆ Cℋ ↔ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ⊆ Cℋ ) )
4 neeq1 ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ( 𝐴 ≠ ∅ ↔ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ≠ ∅ ) )
5 3 4 anbi12d ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) ↔ ( if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ⊆ Cℋ ∧ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ≠ ∅ ) ) )
6 sseq1 ⊢ ( Cℋ = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ( Cℋ ⊆ Cℋ ↔ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ⊆ Cℋ ) )
7 neeq1 ⊢ ( Cℋ = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ( Cℋ ≠ ∅ ↔ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ≠ ∅ ) )
8 6 7 anbi12d ⊢ ( Cℋ = if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) → ( ( Cℋ ⊆ Cℋ ∧ Cℋ ≠ ∅ ) ↔ ( if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ⊆ Cℋ ∧ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , 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 ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ⊆ Cℋ ∧ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ≠ ∅ )
14 13 chintcli ⊢ ∩ if ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Cℋ ) ∈ Cℋ
15 2 14 dedth ⊢ ( ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Cℋ )