Metamath Proof Explorer

Theorem cvrval

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. ( cvbr analog.) (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses cvrfval.b 
|- B = ( Base ` K )
cvrfval.s 
|- .< = ( lt ` K )
cvrfval.c 
|- C = (
Assertion cvrval 
|- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )

Proof

Step Hyp Ref Expression
1 cvrfval.b 
 |-  B = ( Base ` K )
2 cvrfval.s 
 |-  .< = ( lt ` K )
3 cvrfval.c 
 |-  C = (
4 1 2 3 cvrfval 
 |-  ( K e. A -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } )
5 3anass 
 |-  ( ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) <-> ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) )
6 5 opabbii 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) }
7 4 6 eqtrdi 
 |-  ( K e. A -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } )
8 7 breqd 
 |-  ( K e. A -> ( X C Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } Y ) )
9 8 3ad2ant1 
 |-  ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } Y ) )
10 df-br 
 |-  ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } Y <-> <. X , Y >. e. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } )
11 breq1 
 |-  ( x = X -> ( x .< y <-> X .< y ) )
12 breq1 
 |-  ( x = X -> ( x .< z <-> X .< z ) )
13 12 anbi1d 
 |-  ( x = X -> ( ( x .< z /\ z .< y ) <-> ( X .< z /\ z .< y ) ) )
14 13 rexbidv 
 |-  ( x = X -> ( E. z e. B ( x .< z /\ z .< y ) <-> E. z e. B ( X .< z /\ z .< y ) ) )
15 14 notbid 
 |-  ( x = X -> ( -. E. z e. B ( x .< z /\ z .< y ) <-> -. E. z e. B ( X .< z /\ z .< y ) ) )
16 11 15 anbi12d 
 |-  ( x = X -> ( ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) <-> ( X .< y /\ -. E. z e. B ( X .< z /\ z .< y ) ) ) )
17 breq2 
 |-  ( y = Y -> ( X .< y <-> X .< Y ) )
18 breq2 
 |-  ( y = Y -> ( z .< y <-> z .< Y ) )
19 18 anbi2d 
 |-  ( y = Y -> ( ( X .< z /\ z .< y ) <-> ( X .< z /\ z .< Y ) ) )
20 19 rexbidv 
 |-  ( y = Y -> ( E. z e. B ( X .< z /\ z .< y ) <-> E. z e. B ( X .< z /\ z .< Y ) ) )
21 20 notbid 
 |-  ( y = Y -> ( -. E. z e. B ( X .< z /\ z .< y ) <-> -. E. z e. B ( X .< z /\ z .< Y ) ) )
22 17 21 anbi12d 
 |-  ( y = Y -> ( ( X .< y /\ -. E. z e. B ( X .< z /\ z .< y ) ) <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )
23 16 22 opelopab2 
 |-  ( ( X e. B /\ Y e. B ) -> ( <. X , Y >. e. { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )
24 10 23 syl5bb 
 |-  ( ( X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } Y <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )
25 24 3adant1 
 |-  ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } Y <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )
26 9 25 bitrd 
 |-  ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )