Metamath Proof Explorer


Theorem mdbr2

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 ACBCA𝑀BxCxBxABxAB

Proof

Step Hyp Ref Expression
1 mdbr ACBCA𝑀BxCxBxAB=xAB
2 chub1 xCACxxA
3 2 ancoms ACxCxxA
4 iba xBxxAxxAxB
5 ssin xxAxBxxAB
6 4 5 bitrdi xBxxAxxAB
7 3 6 syl5ibcom ACxCxBxxAB
8 chub2 ACxCAxA
9 8 ssrind ACxCABxAB
10 7 9 jctird ACxCxBxxABABxAB
11 10 adantlr ACBCxCxBxxABABxAB
12 simpr ACBCxCxC
13 chincl ACBCABC
14 13 adantr ACBCxCABC
15 chjcl xCACxAC
16 15 ancoms ACxCxAC
17 chincl xACBCxABC
18 16 17 sylan ACxCBCxABC
19 18 an32s ACBCxCxABC
20 chlub xCABCxABCxxABABxABxABxAB
21 12 14 19 20 syl3anc ACBCxCxxABABxABxABxAB
22 11 21 sylibd ACBCxCxBxABxAB
23 eqss xAB=xABxABxABxABxAB
24 23 rbaib xABxABxAB=xABxABxAB
25 22 24 syl6 ACBCxCxBxAB=xABxABxAB
26 25 pm5.74d ACBCxCxBxAB=xABxBxABxAB
27 26 ralbidva ACBCxCxBxAB=xABxCxBxABxAB
28 1 27 bitrd ACBCA𝑀BxCxBxABxAB