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

Metamath Proof Explorer

Theorem cvbr4i

Description: An alternate way to express the covering property. (Contributed by NM, 30-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 
|- A e. CH
chpssat.2 
|- B e. CH
Assertion cvbr4i 
|- ( A  ( A C. B /\ E. x e. HAtoms ( A vH x ) = B ) )

Proof

Step Hyp Ref Expression
1 chpssat.1 
 |-  A e. CH
2 chpssat.2 
 |-  B e. CH
3 cvpss 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  A C. B ) )
4 1 2 3 mp2an 
 |-  ( A  A C. B )
5 1 2 cvati 
 |-  ( A  E. x e. HAtoms ( A vH x ) = B )
6 4 5 jca 
 |-  ( A  ( A C. B /\ E. x e. HAtoms ( A vH x ) = B ) )
7 chcv2 
 |-  ( ( A e. CH /\ x e. HAtoms ) -> ( A C. ( A vH x ) <-> A
8 1 7 mpan 
 |-  ( x e. HAtoms -> ( A C. ( A vH x ) <-> A
9 8 adantr 
 |-  ( ( x e. HAtoms /\ ( A vH x ) = B ) -> ( A C. ( A vH x ) <-> A
10 psseq2 
 |-  ( ( A vH x ) = B -> ( A C. ( A vH x ) <-> A C. B ) )
11 10 adantl 
 |-  ( ( x e. HAtoms /\ ( A vH x ) = B ) -> ( A C. ( A vH x ) <-> A C. B ) )
12 breq2 
 |-  ( ( A vH x ) = B -> ( A  A
13 12 adantl 
 |-  ( ( x e. HAtoms /\ ( A vH x ) = B ) -> ( A  A
14 9 11 13 3bitr3d 
 |-  ( ( x e. HAtoms /\ ( A vH x ) = B ) -> ( A C. B <-> A
15 14 biimpd 
 |-  ( ( x e. HAtoms /\ ( A vH x ) = B ) -> ( A C. B -> A
16 15 ex 
 |-  ( x e. HAtoms -> ( ( A vH x ) = B -> ( A C. B -> A
17 16 com3r 
 |-  ( A C. B -> ( x e. HAtoms -> ( ( A vH x ) = B -> A
18 17 rexlimdv 
 |-  ( A C. B -> ( E. x e. HAtoms ( A vH x ) = B -> A
19 18 imp 
 |-  ( ( A C. B /\ E. x e. HAtoms ( A vH x ) = B ) -> A
20 6 19 impbii 
 |-  ( A  ( A C. B /\ E. x e. HAtoms ( A vH x ) = B ) )