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

Metamath Proof Explorer

Theorem dmdbr

Description: Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ Cℋ ↔ 𝐴 ∈ Cℋ ) )
2 1 anbi1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ↔ ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ) )
3 ineq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ 𝐴 ) )
4 3 oveq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∩ 𝑦 ) ∨ℋ 𝑧 ) = ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) )
5 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∨ℋ 𝑧 ) = ( 𝐴 ∨ℋ 𝑧 ) )
6 5 ineq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∩ ( 𝑦 ∨ℋ 𝑧 ) ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) )
7 4 6 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑥 ∩ 𝑦 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝑦 ∨ℋ 𝑧 ) ) ↔ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ) )
8 7 imbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝑦 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝑦 ∨ℋ 𝑧 ) ) ) ↔ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ) ) )
9 8 ralbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ Cℋ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝑦 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝑦 ∨ℋ 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ) ) )
10 2 9 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝑦 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝑦 ∨ℋ 𝑧 ) ) ) ) ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ) ) ) )
11 eleq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ Cℋ ↔ 𝐵 ∈ Cℋ ) )
12 11 anbi2d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ↔ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) )
13 sseq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑥 ) )
14 oveq2 ⊢ ( 𝑧 = 𝐵 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
15 oveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 ∨ℋ 𝑧 ) = ( 𝐴 ∨ℋ 𝐵 ) )
16 15 ineq2d ⊢ ( 𝑧 = 𝐵 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
17 14 16 eqeq12d ⊢ ( 𝑧 = 𝐵 → ( ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ↔ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
18 13 17 imbi12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ) ↔ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
19 18 ralbidv ⊢ ( 𝑧 = 𝐵 → ( ∀ 𝑥 ∈ Cℋ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
20 12 19 anbi12d ⊢ ( 𝑧 = 𝐵 → ( ( ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝑧 ) ) ) ) ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
21 df-dmd ⊢ 𝑀ℋ* = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝑦 ) ∨ℋ 𝑧 ) = ( 𝑥 ∩ ( 𝑦 ∨ℋ 𝑧 ) ) ) ) }
22 10 20 21 brabg ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
23 22 bianabs ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )