Metamath Proof Explorer

Theorem mddmd2

Description: Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mddmd2 ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 𝑀ℋ 𝑥 ↔ 𝐴 𝑀ℋ 𝑦 ) )
2 1 cbvralvw ⊢ ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑦 ∈ Cℋ 𝐴 𝑀ℋ 𝑦 )
3 mdbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝑦 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) ) )
4 chjcom ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ 𝐴 ) )
5 4 ineq1d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∩ 𝑦 ) = ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) )
6 incom ⊢ ( ( 𝐴 ∨ℋ 𝑥 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) )
7 5 6 eqtr3di ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) )
8 7 adantlr ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) )
9 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 ∩ 𝑦 ) ∈ Cℋ )
10 chjcom ⊢ ( ( ( 𝐴 ∩ 𝑦 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝑦 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) )
11 9 10 sylan ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝑦 ) ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) )
12 incom ⊢ ( 𝐴 ∩ 𝑦 ) = ( 𝑦 ∩ 𝐴 )
13 12 oveq1i ⊢ ( ( 𝐴 ∩ 𝑦 ) ∨ℋ 𝑥 ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 )
14 11 13 eqtr3di ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) )
15 8 14 eqeq12d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ↔ ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) ) )
16 eqcom ⊢ ( ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) = ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) ↔ ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) )
17 15 16 bitrdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ↔ ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) )
18 17 imbi2d ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ⊆ 𝑦 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) ↔ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
19 18 ralbidva ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑦 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
20 3 19 bitrd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝑦 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
21 20 ralbidva ⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ 𝐴 𝑀ℋ 𝑦 ↔ ∀ 𝑦 ∈ Cℋ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
22 2 21 bitrid ⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑦 ∈ Cℋ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
23 ralcom ⊢ ( ∀ 𝑦 ∈ Cℋ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) )
24 22 23 bitrdi ⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
25 dmdbr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝑥 ↔ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
26 25 ralbidva ⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ↔ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∨ℋ 𝑥 ) ) ) ) )
27 24 26 bitr4d ⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ) )