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

Metamath Proof Explorer

Theorem mdslmd1lem3

Description: Lemma for mdslmd1i . (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdslmd.1 ⊢ 𝐴 ∈ Cℋ
mdslmd.2 ⊢ 𝐵 ∈ Cℋ
mdslmd.3 ⊢ 𝐶 ∈ Cℋ
mdslmd.4 ⊢ 𝐷 ∈ Cℋ
Assertion mdslmd1lem3 ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdslmd.1 ⊢ 𝐴 ∈ Cℋ
2 mdslmd.2 ⊢ 𝐵 ∈ Cℋ
3 mdslmd.3 ⊢ 𝐶 ∈ Cℋ
4 mdslmd.4 ⊢ 𝐷 ∈ Cℋ
5 oveq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( 𝑥 ∨ℋ 𝐴 ) = ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) )
6 5 sseq1d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 ↔ ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ⊆ 𝐷 ) )
7 5 oveq1d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) = ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) )
8 7 ineq1d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) = ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) )
9 5 oveq1d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) = ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
10 8 9 sseq12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
11 6 10 imbi12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ↔ ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
12 sseq2 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ↔ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ) )
13 sseq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ↔ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ ( 𝐷 ∩ 𝐵 ) ) )
14 12 13 anbi12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) ↔ ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ ( 𝐷 ∩ 𝐵 ) ) ) )
15 oveq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) = ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
16 15 ineq1d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
17 oveq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) = ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) )
18 16 17 sseq12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ↔ ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
19 14 18 imbi12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ↔ ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
20 11 19 imbi12d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) ↔ ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) ) )
21 20 imbi2d ⊢ ( 𝑥 = if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) → ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) ) ↔ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) ) ) )
22 h0elch ⊢ 0ℋ ∈ Cℋ
23 22 elimel ⊢ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∈ Cℋ
24 1 2 3 4 23 mdslmd1lem1 ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∧ if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( if ( 𝑥 ∈ Cℋ , 𝑥 , 0ℋ ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
25 21 24 dedth ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) ) )
26 25 imp ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )