Description: Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr . (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | mdbr2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mdbr | |
|
2 | chub1 | |
|
3 | 2 | ancoms | |
4 | iba | |
|
5 | ssin | |
|
6 | 4 5 | bitrdi | |
7 | 3 6 | syl5ibcom | |
8 | chub2 | |
|
9 | 8 | ssrind | |
10 | 7 9 | jctird | |
11 | 10 | adantlr | |
12 | simpr | |
|
13 | chincl | |
|
14 | 13 | adantr | |
15 | chjcl | |
|
16 | 15 | ancoms | |
17 | chincl | |
|
18 | 16 17 | sylan | |
19 | 18 | an32s | |
20 | chlub | |
|
21 | 12 14 19 20 | syl3anc | |
22 | 11 21 | sylibd | |
23 | eqss | |
|
24 | 23 | rbaib | |
25 | 22 24 | syl6 | |
26 | 25 | pm5.74d | |
27 | 26 | ralbidva | |
28 | 1 27 | bitrd | |