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

Metamath Proof Explorer

Theorem mdbr

Description: Binary relation expressing <. A , B >. is a modular pair. Definition 1.1 of MaedaMaeda p. 1. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ Cℋ ↔ 𝐴 ∈ Cℋ ) )
2 1 anbi1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ↔ ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ) )
3 oveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∨ℋ 𝑦 ) = ( 𝑥 ∨ℋ 𝐴 ) )
4 3 ineq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∨ℋ 𝑦 ) ∩ 𝑧 ) = ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑧 ) )
5 ineq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∩ 𝑧 ) = ( 𝐴 ∩ 𝑧 ) )
6 5 oveq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∨ℋ ( 𝑦 ∩ 𝑧 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑧 ) ) )
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 sseq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑥 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝐵 ) )
14 ineq2 ⊢ ( 𝑧 = 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝑧 ) = ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
15 ineq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 ∩ 𝑧 ) = ( 𝐴 ∩ 𝐵 ) )
16 15 oveq2d ⊢ ( 𝑧 = 𝐵 → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝑧 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
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-md ⊢ 𝑀ℋ = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝑧 → ( ( 𝑥 ∨ℋ 𝑦 ) ∩ 𝑧 ) = ( 𝑥 ∨ℋ ( 𝑦 ∩ 𝑧 ) ) ) ) }
22 10 20 21 brabg ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) ) )
23 22 bianabs ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )