Metamath Proof Explorer


Theorem mdcompli

Description: A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of MaedaMaeda p. 4. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdcompl.1 AC
mdcompl.2 BC
Assertion mdcompli A𝑀BAAB𝑀BAB

Proof

Step Hyp Ref Expression
1 mdcompl.1 AC
2 mdcompl.2 BC
3 1 2 chincli ABC
4 3 mdoc1i AB𝑀AB
5 3 dmdoc2i AB𝑀*AB
6 ssid ABAB
7 1 2 chjcli ABC
8 7 chssii AB
9 3 chjoi ABAB=
10 8 9 sseqtrri ABABAB
11 3 choccli ABC
12 3 11 1 2 mdslmd1i AB𝑀ABAB𝑀*ABABABABABABA𝑀BAAB𝑀BAB
13 4 5 6 10 12 mp4an A𝑀BAAB𝑀BAB