This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
2 chub1 ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
3 2 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
4 iba ⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐴 ) ↔ ( 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐴 ) ∧ 𝑥 ⊆ 𝐵 ) ) )
5 ssin ⊢ ( ( 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐴 ) ∧ 𝑥 ⊆ 𝐵 ) ↔ 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
6 4 5 bitrdi ⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ⊆ ( 𝑥 ∨ℋ 𝐴 ) ↔ 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
7 3 6 syl5ibcom ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
8 chub2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → 𝐴 ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
9 8 ssrind ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
10 7 9 jctird ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 → ( 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
11 10 adantlr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 → ( 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
12 simpr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → 𝑥 ∈ Cℋ )
13 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
14 13 adantr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
15 chjcl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑥 ∨ℋ 𝐴 ) ∈ Cℋ )
16 15 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∨ℋ 𝐴 ) ∈ Cℋ )
17 chincl ⊢ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ )
18 16 17 sylan ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ 𝐵 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ )
19 18 an32s ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ )
20 chlub ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ ) → ( ( 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
21 12 14 19 20 syl3anc ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ↔ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
22 11 21 sylibd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
23 eqss ⊢ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
24 23 rbaib ⊢ ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
25 22 24 syl6 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
26 25 pm5.74d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
27 26 ralbidva ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
28 1 27 bitrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )