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

Theorem cvrval 30004
 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 23777 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
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvrfval.b . . . . . 6
2 cvrfval.s . . . . . 6
3 cvrfval.c . . . . . 6
41, 2, 3cvrfval 30003 . . . . 5
5 3anass 940 . . . . . 6
65opabbii 4264 . . . . 5
74, 6syl6eq 2483 . . . 4
87breqd 4215 . . 3
10 df-br 4205 . . . 4
11 breq1 4207 . . . . . 6
12 breq1 4207 . . . . . . . . 9
1312anbi1d 686 . . . . . . . 8
1413rexbidv 2718 . . . . . . 7
1514notbid 286 . . . . . 6
1611, 15anbi12d 692 . . . . 5
17 breq2 4208 . . . . . 6
18 breq2 4208 . . . . . . . . 9
1918anbi2d 685 . . . . . . . 8
2019rexbidv 2718 . . . . . . 7
2120notbid 286 . . . . . 6
2217, 21anbi12d 692 . . . . 5
2316, 22opelopab2 4467 . . . 4
2410, 23syl5bb 249 . . 3