# Metamath Proof Explorer

## Theorem csmdsymi

Description: Cross-symmetry implies M-symmetry. Theorem 1.9.1 of MaedaMaeda p. 3. (Contributed by NM, 24-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses csmdsym.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
csmdsym.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion csmdsymi ${⊢}\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\to {B}{𝑀}_{ℋ}{A}$

### Proof

Step Hyp Ref Expression
1 csmdsym.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 csmdsym.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 incom ${⊢}{A}\cap {B}={B}\cap {A}$
4 3 sseq1i ${⊢}{A}\cap {B}\subseteq {x}↔{B}\cap {A}\subseteq {x}$
5 4 biimpri ${⊢}{B}\cap {A}\subseteq {x}\to {A}\cap {B}\subseteq {x}$
6 chjcom ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {x}{\vee }_{ℋ}{B}={B}{\vee }_{ℋ}{x}$
7 2 6 mpan2 ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {x}{\vee }_{ℋ}{B}={B}{\vee }_{ℋ}{x}$
8 7 ineq1d ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}=\left({B}{\vee }_{ℋ}{x}\right)\cap {A}$
9 incom ${⊢}\left({B}{\vee }_{ℋ}{x}\right)\cap {A}={A}\cap \left({B}{\vee }_{ℋ}{x}\right)$
10 8 9 syl6eq ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}={A}\cap \left({B}{\vee }_{ℋ}{x}\right)$
11 10 ad2antlr ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}={A}\cap \left({B}{\vee }_{ℋ}{x}\right)$
12 2 a1i ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {B}\in {\mathbf{C}}_{ℋ}$
13 id ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {x}\in {\mathbf{C}}_{ℋ}$
14 1 a1i ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {A}\in {\mathbf{C}}_{ℋ}$
15 12 13 14 3jca ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)$
16 15 ad2antlr ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to \left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)$
17 inss2 ${⊢}{A}\cap {B}\subseteq {B}$
18 ssid ${⊢}{B}\subseteq {B}$
19 17 18 pm3.2i ${⊢}\left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)$
20 sseq2 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({A}\cap {B}\subseteq {x}↔{A}\cap {B}\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\right)$
21 sseq1 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({x}\subseteq {A}↔if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {A}\right)$
22 20 21 anbi12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)↔\left({A}\cap {B}\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {A}\right)\right)$
23 22 3anbi2d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\wedge \left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)\right)↔\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {A}\right)\wedge \left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)\right)\right)$
24 breq1 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({x}{𝑀}_{ℋ}{B}↔if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){𝑀}_{ℋ}{B}\right)$
25 23 24 imbi12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\left(\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\wedge \left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)\right)\to {x}{𝑀}_{ℋ}{B}\right)↔\left(\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {A}\right)\wedge \left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)\right)\to if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){𝑀}_{ℋ}{B}\right)\right)$
26 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
27 26 elimel ${⊢}if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
28 1 2 27 2 mdslmd4i ${⊢}\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {A}\right)\wedge \left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)\right)\to if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){𝑀}_{ℋ}{B}$
29 25 28 dedth ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left(\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\wedge \left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)\right)\to {x}{𝑀}_{ℋ}{B}\right)$
30 29 com12 ${⊢}\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\wedge \left({A}\cap {B}\subseteq {B}\wedge {B}\subseteq {B}\right)\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to {x}{𝑀}_{ℋ}{B}\right)$
31 19 30 mp3an3 ${⊢}\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to {x}{𝑀}_{ℋ}{B}\right)$
32 31 imp ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {x}{𝑀}_{ℋ}{B}$
33 32 an32s ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to {x}{𝑀}_{ℋ}{B}$
34 33 adantlll ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to {x}{𝑀}_{ℋ}{B}$
35 breq1 ${⊢}{c}={x}\to \left({c}{𝑀}_{ℋ}{B}↔{x}{𝑀}_{ℋ}{B}\right)$
36 breq2 ${⊢}{c}={x}\to \left({B}{𝑀}_{ℋ}^{*}{c}↔{B}{𝑀}_{ℋ}^{*}{x}\right)$
37 35 36 imbi12d ${⊢}{c}={x}\to \left(\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)↔\left({x}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{x}\right)\right)$
38 37 rspccva ${⊢}\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{x}\right)$
39 38 adantlr ${⊢}\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{x}\right)$
40 39 adantr ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to \left({x}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{x}\right)$
41 34 40 mpd ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to {B}{𝑀}_{ℋ}^{*}{x}$
42 simprr ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to {x}\subseteq {A}$
43 dmdi ${⊢}\left(\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({B}{𝑀}_{ℋ}^{*}{x}\wedge {x}\subseteq {A}\right)\right)\to \left({A}\cap {B}\right){\vee }_{ℋ}{x}={A}\cap \left({B}{\vee }_{ℋ}{x}\right)$
44 16 41 42 43 syl12anc ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to \left({A}\cap {B}\right){\vee }_{ℋ}{x}={A}\cap \left({B}{\vee }_{ℋ}{x}\right)$
45 1 2 chincli ${⊢}{A}\cap {B}\in {\mathbf{C}}_{ℋ}$
46 chjcom ${⊢}\left({A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\cap {B}\right){\vee }_{ℋ}{x}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)$
47 45 46 mpan ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left({A}\cap {B}\right){\vee }_{ℋ}{x}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)$
48 3 oveq2i ${⊢}{x}{\vee }_{ℋ}\left({A}\cap {B}\right)={x}{\vee }_{ℋ}\left({B}\cap {A}\right)$
49 47 48 syl6eq ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left({A}\cap {B}\right){\vee }_{ℋ}{x}={x}{\vee }_{ℋ}\left({B}\cap {A}\right)$
50 49 ad2antlr ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to \left({A}\cap {B}\right){\vee }_{ℋ}{x}={x}{\vee }_{ℋ}\left({B}\cap {A}\right)$
51 11 44 50 3eqtr2d ${⊢}\left(\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}={x}{\vee }_{ℋ}\left({B}\cap {A}\right)$
52 51 ex ${⊢}\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}={x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)$
53 5 52 sylani ${⊢}\left(\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({B}\cap {A}\subseteq {x}\wedge {x}\subseteq {A}\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}={x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)$
54 53 ralrimiva ${⊢}\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({B}\cap {A}\subseteq {x}\wedge {x}\subseteq {A}\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}={x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)$
55 2 1 mdsl2bi ${⊢}{B}{𝑀}_{ℋ}{A}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({B}\cap {A}\subseteq {x}\wedge {x}\subseteq {A}\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}={x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)$
56 54 55 sylibr ${⊢}\left(\forall {c}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({c}{𝑀}_{ℋ}{B}\to {B}{𝑀}_{ℋ}^{*}{c}\right)\wedge {A}{𝑀}_{ℋ}{B}\right)\to {B}{𝑀}_{ℋ}{A}$