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ℋ )