Theorem dmdi4

Description: Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	dmdi4	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 → ( ( 𝐶 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmdbr4	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
2	1	biimpd	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 → ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
3		oveq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∨ℋ 𝐵 ) = ( 𝐶 ∨ℋ 𝐵 ) )
4	3	ineq1d	⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐶 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
5	3	ineq1d	⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) = ( ( 𝐶 ∨ℋ 𝐵 ) ∩ 𝐴 ) )
6	5	oveq1d	⊢ ( 𝑥 = 𝐶 → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) = ( ( ( 𝐶 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
7	4 6	sseq12d	⊢ ( 𝑥 = 𝐶 → ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ↔ ( ( 𝐶 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
8	7	rspcv	⊢ ( 𝐶 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( ( 𝐶 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
9	2 8	sylan9	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 → ( ( 𝐶 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
10	9	3impa	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 → ( ( 𝐶 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝐶 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )