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

Metamath Proof Explorer

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_ℋ ) → ( 𝐴 𝑀_ℋ^* 𝐵 → ( ( 𝐶 ∨_ℋ 𝐵 ) ∩ ( 𝐴 ∨_ℋ 𝐵 ) ) ⊆ ( ( ( 𝐶 ∨_ℋ 𝐵 ) ∩ 𝐴 ) ∨_ℋ 𝐵 ) ) )