Metamath Proof Explorer

Theorem mdslmd1lem4

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 mdslmd1lem4 ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdslmd.1 ⊢ 𝐴 ∈ Cℋ
2 mdslmd.2 ⊢ 𝐵 ∈ Cℋ
3 mdslmd.3 ⊢ 𝐶 ∈ Cℋ
4 mdslmd.4 ⊢ 𝐷 ∈ Cℋ
5 ineq1 ⊢ ( 𝑥 = 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 mdslmd1lem2 ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 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ℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )