# 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 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 mdbr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
2 chub1 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {x}\subseteq {x}{\vee }_{ℋ}{A}$
3 2 ancoms ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {x}\subseteq {x}{\vee }_{ℋ}{A}$
4 iba ${⊢}{x}\subseteq {B}\to \left({x}\subseteq {x}{\vee }_{ℋ}{A}↔\left({x}\subseteq {x}{\vee }_{ℋ}{A}\wedge {x}\subseteq {B}\right)\right)$
5 ssin ${⊢}\left({x}\subseteq {x}{\vee }_{ℋ}{A}\wedge {x}\subseteq {B}\right)↔{x}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}$
6 4 5 syl6bb ${⊢}{x}\subseteq {B}\to \left({x}\subseteq {x}{\vee }_{ℋ}{A}↔{x}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)$
7 3 6 syl5ibcom ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\subseteq {B}\to {x}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)$
8 chub2 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {x}{\vee }_{ℋ}{A}$
9 8 ssrind ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}$
10 7 9 jctird ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\subseteq {B}\to \left({x}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\wedge {A}\cap {B}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)\right)$
11 10 adantlr ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\subseteq {B}\to \left({x}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\wedge {A}\cap {B}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)\right)$
12 simpr ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {x}\in {\mathbf{C}}_{ℋ}$
13 chincl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\in {\mathbf{C}}_{ℋ}$
14 13 adantr ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\in {\mathbf{C}}_{ℋ}$
15 chjcl ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {x}{\vee }_{ℋ}{A}\in {\mathbf{C}}_{ℋ}$
16 15 ancoms ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {x}{\vee }_{ℋ}{A}\in {\mathbf{C}}_{ℋ}$
17 chincl ${⊢}\left({x}{\vee }_{ℋ}{A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\in {\mathbf{C}}_{ℋ}$
18 16 17 sylan ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\in {\mathbf{C}}_{ℋ}$
19 18 an32s ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\in {\mathbf{C}}_{ℋ}$
20 chlub ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({x}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\wedge {A}\cap {B}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)↔{x}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)$
21 12 14 19 20 syl3anc ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({x}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\wedge {A}\cap {B}\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)↔{x}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)$
22 11 21 sylibd ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\subseteq {B}\to {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)$
23 eqss ${⊢}\left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)↔\left(\left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\right)$
24 23 rbaib ${⊢}{x}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\to \left(\left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)↔\left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
25 22 24 syl6 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\subseteq {B}\to \left(\left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)↔\left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
26 25 pm5.74d ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)↔\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
27 26 ralbidva ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
28 1 27 bitrd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$