Metamath Proof Explorer

Theorem dmdbr2

Description: Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr . (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion dmdbr2 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 dmdbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
2 chincl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑥 ∩ 𝐴 ) ∈ Cℋ )
3 2 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∩ 𝐴 ) ∈ Cℋ )
4 3 adantlr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∩ 𝐴 ) ∈ Cℋ )
5 simplr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → 𝐵 ∈ Cℋ )
6 simpr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → 𝑥 ∈ Cℋ )
7 inss1 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥
8 chlub ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝐵 ⊆ 𝑥 ) ↔ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ 𝑥 ) )
9 8 biimpd ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ∧ 𝐵 ⊆ 𝑥 ) → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ 𝑥 ) )
10 7 9 mpani ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ 𝑥 ) )
11 4 5 6 10 syl3anc ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ 𝑥 ) )
12 simpll ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → 𝐴 ∈ Cℋ )
13 inss2 ⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴
14 chlej1 ⊢ ( ( ( ( 𝑥 ∩ 𝐴 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ) → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
15 13 14 mpan2 ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
16 4 12 5 15 syl3anc ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
17 11 16 jctird ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 → ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ 𝑥 ∧ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
18 ssin ⊢ ( ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ 𝑥 ∧ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
19 17 18 imbitrdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
20 eqss ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
21 20 baib ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ⊆ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
22 19 21 syl6 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝐵 ⊆ 𝑥 → ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
23 22 pm5.74d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ↔ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
24 23 ralbidva ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
25 1 24 bitrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )