Metamath Proof Explorer

Theorem cvbr

Description: Binary relation expressing B covers A , which means that B is larger than A and there is nothing in between. Definition 3.2.18 of PtakPulmannova p. 68. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvbr 
|- ( ( A e. CH /\ B e. CH ) -> ( A  ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( y = A -> ( y e. CH <-> A e. CH ) )
2 1 anbi1d 
 |-  ( y = A -> ( ( y e. CH /\ z e. CH ) <-> ( A e. CH /\ z e. CH ) ) )
3 psseq1 
 |-  ( y = A -> ( y C. z <-> A C. z ) )
4 psseq1 
 |-  ( y = A -> ( y C. x <-> A C. x ) )
5 4 anbi1d 
 |-  ( y = A -> ( ( y C. x /\ x C. z ) <-> ( A C. x /\ x C. z ) ) )
6 5 rexbidv 
 |-  ( y = A -> ( E. x e. CH ( y C. x /\ x C. z ) <-> E. x e. CH ( A C. x /\ x C. z ) ) )
7 6 notbid 
 |-  ( y = A -> ( -. E. x e. CH ( y C. x /\ x C. z ) <-> -. E. x e. CH ( A C. x /\ x C. z ) ) )
8 3 7 anbi12d 
 |-  ( y = A -> ( ( y C. z /\ -. E. x e. CH ( y C. x /\ x C. z ) ) <-> ( A C. z /\ -. E. x e. CH ( A C. x /\ x C. z ) ) ) )
9 2 8 anbi12d 
 |-  ( y = A -> ( ( ( y e. CH /\ z e. CH ) /\ ( y C. z /\ -. E. x e. CH ( y C. x /\ x C. z ) ) ) <-> ( ( A e. CH /\ z e. CH ) /\ ( A C. z /\ -. E. x e. CH ( A C. x /\ x C. z ) ) ) ) )
10 eleq1 
 |-  ( z = B -> ( z e. CH <-> B e. CH ) )
11 10 anbi2d 
 |-  ( z = B -> ( ( A e. CH /\ z e. CH ) <-> ( A e. CH /\ B e. CH ) ) )
12 psseq2 
 |-  ( z = B -> ( A C. z <-> A C. B ) )
13 psseq2 
 |-  ( z = B -> ( x C. z <-> x C. B ) )
14 13 anbi2d 
 |-  ( z = B -> ( ( A C. x /\ x C. z ) <-> ( A C. x /\ x C. B ) ) )
15 14 rexbidv 
 |-  ( z = B -> ( E. x e. CH ( A C. x /\ x C. z ) <-> E. x e. CH ( A C. x /\ x C. B ) ) )
16 15 notbid 
 |-  ( z = B -> ( -. E. x e. CH ( A C. x /\ x C. z ) <-> -. E. x e. CH ( A C. x /\ x C. B ) ) )
17 12 16 anbi12d 
 |-  ( z = B -> ( ( A C. z /\ -. E. x e. CH ( A C. x /\ x C. z ) ) <-> ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) )
18 11 17 anbi12d 
 |-  ( z = B -> ( ( ( A e. CH /\ z e. CH ) /\ ( A C. z /\ -. E. x e. CH ( A C. x /\ x C. z ) ) ) <-> ( ( A e. CH /\ B e. CH ) /\ ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) ) )
19 df-cv 
 |-  . | ( ( y e. CH /\ z e. CH ) /\ ( y C. z /\ -. E. x e. CH ( y C. x /\ x C. z ) ) ) }
20 9 18 19 brabg 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  ( ( A e. CH /\ B e. CH ) /\ ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) ) )
21 20 bianabs 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) )