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_ CH /\ A =/= (/) ) -> |^| A e. CH )

Proof

Step Hyp Ref Expression
1 inteq 
 |-  ( A = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> |^| A = |^| if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) )
2 1 eleq1d 
 |-  ( A = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> ( |^| A e. CH <-> |^| if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) e. CH ) )
3 sseq1 
 |-  ( A = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> ( A C_ CH <-> if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) C_ CH ) )
4 neeq1 
 |-  ( A = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> ( A =/= (/) <-> if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) =/= (/) ) )
5 3 4 anbi12d 
 |-  ( A = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> ( ( A C_ CH /\ A =/= (/) ) <-> ( if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) C_ CH /\ if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) =/= (/) ) ) )
6 sseq1 
 |-  ( CH = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> ( CH C_ CH <-> if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) C_ CH ) )
7 neeq1 
 |-  ( CH = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> ( CH =/= (/) <-> if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) =/= (/) ) )
8 6 7 anbi12d 
 |-  ( CH = if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) -> ( ( CH C_ CH /\ CH =/= (/) ) <-> ( if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) C_ CH /\ if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) =/= (/) ) ) )
9 ssid 
 |-  CH C_ CH
10 h0elch 
 |-  0H e. CH
11 10 ne0ii 
 |-  CH =/= (/)
12 9 11 pm3.2i 
 |-  ( CH C_ CH /\ CH =/= (/) )
13 5 8 12 elimhyp 
 |-  ( if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) C_ CH /\ if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) =/= (/) )
14 13 chintcli 
 |-  |^| if ( ( A C_ CH /\ A =/= (/) ) , A , CH ) e. CH
15 2 14 dedth 
 |-  ( ( A C_ CH /\ A =/= (/) ) -> |^| A e. CH )