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

Theorem cvrval2 28153
 Description: Binary relation expressing covers . Definition of covers in [Kalmbach] p. 15. (cvbr2 22693 analog.) (Contributed by NM, 16-Nov-2011.)
Hypotheses
Ref Expression
cvrletr.b
cvrletr.l
cvrletr.s
cvrletr.c
Assertion
Ref Expression
cvrval2
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem cvrval2
StepHypRef Expression
1 cvrletr.b . . 3
2 cvrletr.s . . 3
3 cvrletr.c . . 3
41, 2, 3cvrval 28148 . 2
5 iman 415 . . . . . . . 8
6 df-ne 2414 . . . . . . . . 9
76anbi2i 678 . . . . . . . 8
85, 7xchbinxr 304 . . . . . . 7
9 cvrletr.l . . . . . . . . . . . . 13
109, 2pltval 13938 . . . . . . . . . . . 12
11103com23 1162 . . . . . . . . . . 11
12113expa 1156 . . . . . . . . . 10
1312anbi2d 687 . . . . . . . . 9
14 anass 633 . . . . . . . . 9
1513, 14syl6rbbr 257 . . . . . . . 8
1615notbid 287 . . . . . . 7
178, 16syl5bb 250 . . . . . 6
1817ralbidva 2523 . . . . 5
19 ralnex 2517 . . . . 5
2018, 19syl6bb 254 . . . 4
2120anbi2d 687 . . 3