Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvrval Unicode version

Theorem cvrval 28148
 Description: Binary relation expressing covers , which means that is larger than and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68. (cvbr 22692 analog.) (Contributed by NM, 18-Sep-2011.)
Hypotheses
Ref Expression
cvrfval.b
cvrfval.s
cvrfval.c
Assertion
Ref Expression
cvrval
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem cvrval
StepHypRef Expression
1 cvrfval.b . . . . . 6
2 cvrfval.s . . . . . 6
3 cvrfval.c . . . . . 6
41, 2, 3cvrfval 28147 . . . . 5
5 3anass 943 . . . . . 6
65opabbii 3980 . . . . 5
74, 6syl6eq 2301 . . . 4
87breqd 3931 . . 3
10 df-br 3921 . . . 4
11 breq1 3923 . . . . . 6
12 breq1 3923 . . . . . . . . 9
1312anbi1d 688 . . . . . . . 8
1413rexbidv 2528 . . . . . . 7
1514notbid 287 . . . . . 6
1611, 15anbi12d 694 . . . . 5
17 breq2 3924 . . . . . 6
18 breq2 3924 . . . . . . . . 9
1918anbi2d 687 . . . . . . . 8
2019rexbidv 2528 . . . . . . 7
2120notbid 287 . . . . . 6
2217, 21anbi12d 694 . . . . 5
2316, 22opelopab2 4178 . . . 4
2410, 23syl5bb 250 . . 3