Description: Two Hilbert lattice elements have the modular pair property if the first is an atom. Theorem 7.6(b) of MaedaMaeda p. 31. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | atmd | ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → 𝐴 𝑀ℋ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | atdmd | ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝑥 ∈ Cℋ ) → 𝐴 𝑀ℋ* 𝑥 ) | |
| 2 | 1 | ralrimiva | ⊢ ( 𝐴 ∈ HAtoms → ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ) |
| 3 | atelch | ⊢ ( 𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ ) | |
| 4 | mddmd2 | ⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ) ) | |
| 5 | 3 4 | syl | ⊢ ( 𝐴 ∈ HAtoms → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥 ) ) |
| 6 | 2 5 | mpbird | ⊢ ( 𝐴 ∈ HAtoms → ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ) |
| 7 | breq2 | ⊢ ( 𝑥 = 𝐵 → ( 𝐴 𝑀ℋ 𝑥 ↔ 𝐴 𝑀ℋ 𝐵 ) ) | |
| 8 | 7 | rspcv | ⊢ ( 𝐵 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 → 𝐴 𝑀ℋ 𝐵 ) ) |
| 9 | 6 8 | mpan9 | ⊢ ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → 𝐴 𝑀ℋ 𝐵 ) |