Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  dmdbr4 Structured version   Unicode version

Theorem dmdbr4 23840
 Description: Binary relation expressing the dual modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
Assertion
Ref Expression
dmdbr4
Distinct variable groups:   ,   ,

Proof of Theorem dmdbr4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dmdbr2 23837 . 2
2 chub2 23041 . . . . . . . . 9
32ancoms 441 . . . . . . . 8
4 chjcl 22890 . . . . . . . . 9
5 sseq2 3356 . . . . . . . . . . 11
6 ineq1 3521 . . . . . . . . . . . 12
7 ineq1 3521 . . . . . . . . . . . . 13
87oveq1d 6125 . . . . . . . . . . . 12
96, 8sseq12d 3363 . . . . . . . . . . 11
105, 9imbi12d 313 . . . . . . . . . 10
1110rspcv 3054 . . . . . . . . 9
124, 11syl 16 . . . . . . . 8
133, 12mpid 40 . . . . . . 7
1413ex 425 . . . . . 6
1514com3l 78 . . . . 5
1615ralrimdv 2801 . . . 4
17 chlejb2 23046 . . . . . . . . . . . 12
1817biimpa 472 . . . . . . . . . . 11
1918ineq1d 3527 . . . . . . . . . 10
2018ineq1d 3527 . . . . . . . . . . 11
2120oveq1d 6125 . . . . . . . . . 10
2219, 21sseq12d 3363 . . . . . . . . 9
2322biimpd 200 . . . . . . . 8
2423ex 425 . . . . . . 7
2524com23 75 . . . . . 6
2625ralimdva 2790 . . . . 5
27 sseq2 3356 . . . . . . 7
28 ineq1 3521 . . . . . . . 8
29 ineq1 3521 . . . . . . . . 9
3029oveq1d 6125 . . . . . . . 8
3128, 30sseq12d 3363 . . . . . . 7
3227, 31imbi12d 313 . . . . . 6
3332cbvralv 2938 . . . . 5
3426, 33syl6ib 219 . . . 4
3516, 34impbid 185 . . 3