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