Theorem mdslmd1lem1 30378

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

Hypotheses

Ref	Expression
mdslmd.1	⊢ 𝐴 ∈ Cℋ
mdslmd.2	⊢ 𝐵 ∈ Cℋ
mdslmd.3	⊢ 𝐶 ∈ Cℋ
mdslmd.4	⊢ 𝐷 ∈ Cℋ
mdslmd1lem.5	⊢ 𝑅 ∈ Cℋ

Assertion

Ref	Expression
mdslmd1lem1	⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))

Proof of Theorem mdslmd1lem1

Step	Hyp	Ref	Expression
1		mdslmd1lem.5	. . . . . 6 ⊢ 𝑅 ∈ Cℋ
2		mdslmd.4	. . . . . . 7 ⊢ 𝐷 ∈ Cℋ
3		mdslmd.2	. . . . . . 7 ⊢ 𝐵 ∈ Cℋ
4	2, 3	chincli 29513	. . . . . 6 ⊢ (𝐷 ∩ 𝐵) ∈ Cℋ
5		mdslmd.1	. . . . . 6 ⊢ 𝐴 ∈ Cℋ
6	1, 4, 5	chlej1i 29526	. . . . 5 ⊢ (𝑅 ⊆ (𝐷 ∩ 𝐵) → (𝑅 ∨ℋ 𝐴) ⊆ ((𝐷 ∩ 𝐵) ∨ℋ 𝐴))
7		simpr 488	. . . . . . . 8 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) → 𝐵 𝑀ℋ* 𝐴)
8		simpr 488	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) → 𝐴 ⊆ 𝐷)
9		simpr 488	. . . . . . . 8 ⊢ ((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))
10	5, 3, 2	3pm3.2i 1341	. . . . . . . . 9 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
11		dmdsl3 30368	. . . . . . . . 9 ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) = 𝐷)
12	10, 11	mpan 690	. . . . . . . 8 ⊢ ((𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) = 𝐷)
13	7, 8, 9, 12	syl3an 1162	. . . . . . 7 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) = 𝐷)
14	13	3expb 1122	. . . . . 6 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) = 𝐷)
15	14	sseq2d 3923	. . . . 5 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → ((𝑅 ∨ℋ 𝐴) ⊆ ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) ↔ (𝑅 ∨ℋ 𝐴) ⊆ 𝐷))
16	6, 15	syl5ib 247	. . . 4 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (𝑅 ⊆ (𝐷 ∩ 𝐵) → (𝑅 ∨ℋ 𝐴) ⊆ 𝐷))
17	16	adantld 494	. . 3 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → (𝑅 ∨ℋ 𝐴) ⊆ 𝐷))
18	17	imim1d 82	. 2 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)))))
19		simpll 767	. . . . . . . . . 10 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴))
20		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝐴 ⊆ 𝐶)
21	20	ad2antlr 727	. . . . . . . . . . . 12 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 ⊆ 𝐶)
22	5, 1	chub2i 29523	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (𝑅 ∨ℋ 𝐴)
23	21, 22	jctil 523	. . . . . . . . . . 11 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ⊆ (𝑅 ∨ℋ 𝐴) ∧ 𝐴 ⊆ 𝐶))
24		ssin 4135	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ (𝑅 ∨ℋ 𝐴) ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∩ 𝐶))
25	23, 24	sylib 221	. . . . . . . . . 10 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∩ 𝐶))
26		inss1 4133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∩ 𝐵) ⊆ 𝐷
27		sstr 3899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ⊆ (𝐷 ∩ 𝐵) ∧ (𝐷 ∩ 𝐵) ⊆ 𝐷) → 𝑅 ⊆ 𝐷)
28	26, 27	mpan2 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ⊆ (𝐷 ∩ 𝐵) → 𝑅 ⊆ 𝐷)
29		sstr 3899	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵))
30	28, 29	sylan 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ⊆ (𝐷 ∩ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵))
31	30	ancoms 462	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵))
32	31	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵))
33	32	adantll 714	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵))
34	33	ad2ant2l 746	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵))
35	5, 3	chub1i 29522	. . . . . . . . . . . . . 14 ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)
36	34, 35	jctir 524	. . . . . . . . . . . . 13 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝑅 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)))
37	5, 3	chjcli 29510	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
38	1, 5, 37	chlubi 29524	. . . . . . . . . . . . 13 ⊢ ((𝑅 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝑅 ∨ℋ 𝐴) ⊆ (𝐴 ∨ℋ 𝐵))
39	36, 38	sylib 221	. . . . . . . . . . . 12 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝑅 ∨ℋ 𝐴) ⊆ (𝐴 ∨ℋ 𝐵))
40		simprrl 781	. . . . . . . . . . . . 13 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))
41	40	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))
42	39, 41	jca 515	. . . . . . . . . . 11 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ 𝐴) ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵)))
43	1, 5	chjcli 29510	. . . . . . . . . . . 12 ⊢ (𝑅 ∨ℋ 𝐴) ∈ Cℋ
44		mdslmd.3	. . . . . . . . . . . 12 ⊢ 𝐶 ∈ Cℋ
45	43, 44, 37	chlubi 29524	. . . . . . . . . . 11 ⊢ (((𝑅 ∨ℋ 𝐴) ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ⊆ (𝐴 ∨ℋ 𝐵))
46	42, 45	sylib 221	. . . . . . . . . 10 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ⊆ (𝐴 ∨ℋ 𝐵))
47	5, 3, 43, 44	mdslj1i 30372	. . . . . . . . . 10 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∩ 𝐶) ∧ ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ⊆ (𝐴 ∨ℋ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐵) = (((𝑅 ∨ℋ 𝐴) ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)))
48	19, 25, 46, 47	syl12anc 837	. . . . . . . . 9 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐵) = (((𝑅 ∨ℋ 𝐴) ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)))
49		simplll 775	. . . . . . . . . . 11 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 𝑀ℋ 𝐵)
50		simplrl 777	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷))
51		ssin 4135	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ↔ 𝐴 ⊆ (𝐶 ∩ 𝐷))
52	50, 51	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 ⊆ (𝐶 ∩ 𝐷))
53	52	ssrind 4140	. . . . . . . . . . . . 13 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐷) ∩ 𝐵))
54		inindir 4132	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∩ 𝐷) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))
55	53, 54	sseqtrdi 3941	. . . . . . . . . . . 12 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))
56		simprl 771	. . . . . . . . . . . 12 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅)
57	55, 56	sstrd 3901	. . . . . . . . . . 11 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ∩ 𝐵) ⊆ 𝑅)
58		inss2 4134	. . . . . . . . . . . . 13 ⊢ (𝐷 ∩ 𝐵) ⊆ 𝐵
59		sstr 3899	. . . . . . . . . . . . 13 ⊢ ((𝑅 ⊆ (𝐷 ∩ 𝐵) ∧ (𝐷 ∩ 𝐵) ⊆ 𝐵) → 𝑅 ⊆ 𝐵)
60	58, 59	mpan2 691	. . . . . . . . . . . 12 ⊢ (𝑅 ⊆ (𝐷 ∩ 𝐵) → 𝑅 ⊆ 𝐵)
61	60	ad2antll 729	. . . . . . . . . . 11 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝑅 ⊆ 𝐵)
62	5, 3, 1	3pm3.2i 1341	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑅 ∈ Cℋ )
63		mdsl3 30369	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑅 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐵)) → ((𝑅 ∨ℋ 𝐴) ∩ 𝐵) = 𝑅)
64	62, 63	mpan 690	. . . . . . . . . . 11 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐵) → ((𝑅 ∨ℋ 𝐴) ∩ 𝐵) = 𝑅)
65	49, 57, 61, 64	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ 𝐴) ∩ 𝐵) = 𝑅)
66	65	oveq1d 7217	. . . . . . . . 9 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) = (𝑅 ∨ℋ (𝐶 ∩ 𝐵)))
67	48, 66	eqtr2d 2775	. . . . . . . 8 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝑅 ∨ℋ (𝐶 ∩ 𝐵)) = (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐵))
68	67	ineq1d 4116	. . . . . . 7 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) = ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))
69		inindir 4132	. . . . . . 7 ⊢ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) = ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))
70	68, 69	eqtr4di 2792	. . . . . 6 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) = ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵))
71	52, 22	jctil 523	. . . . . . . . 9 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ⊆ (𝑅 ∨ℋ 𝐴) ∧ 𝐴 ⊆ (𝐶 ∩ 𝐷)))
72		ssin 4135	. . . . . . . . 9 ⊢ ((𝐴 ⊆ (𝑅 ∨ℋ 𝐴) ∧ 𝐴 ⊆ (𝐶 ∩ 𝐷)) ↔ 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∩ (𝐶 ∩ 𝐷)))
73	71, 72	sylib 221	. . . . . . . 8 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∩ (𝐶 ∩ 𝐷)))
74		ssinss1 4142	. . . . . . . . . . . 12 ⊢ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) → (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))
75	74	ad2antrl 728	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))
76	75	ad2antlr 727	. . . . . . . . . 10 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))
77	39, 76	jca 515	. . . . . . . . 9 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ 𝐴) ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)))
78	44, 2	chincli 29513	. . . . . . . . . 10 ⊢ (𝐶 ∩ 𝐷) ∈ Cℋ
79	43, 78, 37	chlubi 29524	. . . . . . . . 9 ⊢ (((𝑅 ∨ℋ 𝐴) ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) ↔ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵))
80	77, 79	sylib 221	. . . . . . . 8 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵))
81	5, 3, 43, 78	mdslj1i 30372	. . . . . . . 8 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∩ (𝐶 ∩ 𝐷)) ∧ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵) = (((𝑅 ∨ℋ 𝐴) ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐷) ∩ 𝐵)))
82	19, 73, 80, 81	syl12anc 837	. . . . . . 7 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵) = (((𝑅 ∨ℋ 𝐴) ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐷) ∩ 𝐵)))
83	54	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((𝐶 ∩ 𝐷) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))
84	65, 83	oveq12d 7220	. . . . . . 7 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐷) ∩ 𝐵)) = (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))
85	82, 84	eqtr2d 2775	. . . . . 6 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) = (((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵))
86	70, 85	sseq12d 3924	. . . . 5 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) ↔ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ (((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵)))
87		simpllr 776	. . . . . 6 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐵 𝑀ℋ* 𝐴)
88		simplr 769	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝐴 ⊆ 𝐷)
89	88	ad2antlr 727	. . . . . . . . . 10 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 ⊆ 𝐷)
90	43, 44	chub1i 29522	. . . . . . . . . . 11 ⊢ (𝑅 ∨ℋ 𝐴) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶)
91	22, 90	sstri 3900	. . . . . . . . . 10 ⊢ 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶)
92	89, 91	jctil 523	. . . . . . . . 9 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∧ 𝐴 ⊆ 𝐷))
93		ssin 4135	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∧ 𝐴 ⊆ 𝐷) ↔ 𝐴 ⊆ (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷))
94	92, 93	sylib 221	. . . . . . . 8 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 ⊆ (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷))
95	43, 78	chub1i 29522	. . . . . . . . 9 ⊢ (𝑅 ∨ℋ 𝐴) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))
96	22, 95	sstri 3900	. . . . . . . 8 ⊢ 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))
97	94, 96	jctir 524	. . . . . . 7 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (𝐴 ⊆ (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∧ 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))
98		ssin 4135	. . . . . . 7 ⊢ ((𝐴 ⊆ (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∧ 𝐴 ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) ↔ 𝐴 ⊆ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))
99	97, 98	sylib 221	. . . . . 6 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → 𝐴 ⊆ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))
100		inss2 4134	. . . . . . . . . . 11 ⊢ (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ 𝐷
101		sstr 3899	. . . . . . . . . . 11 ⊢ (((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))
102	100, 101	mpan 690	. . . . . . . . . 10 ⊢ (𝐷 ⊆ (𝐴 ∨ℋ 𝐵) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))
103	102	ad2antll 729	. . . . . . . . 9 ⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))
104	103	ad2antlr 727	. . . . . . . 8 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))
105	104, 80	jca 515	. . . . . . 7 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵) ∧ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵)))
106	43, 44	chjcli 29510	. . . . . . . . 9 ⊢ ((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∈ Cℋ
107	106, 2	chincli 29513	. . . . . . . 8 ⊢ (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∈ Cℋ
108	43, 78	chjcli 29510	. . . . . . . 8 ⊢ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ∈ Cℋ
109	107, 108, 37	chlubi 29524	. . . . . . 7 ⊢ (((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵) ∧ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵)) ↔ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∨ℋ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) ⊆ (𝐴 ∨ℋ 𝐵))
110	105, 109	sylib 221	. . . . . 6 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∨ℋ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) ⊆ (𝐴 ∨ℋ 𝐵))
111	5, 3, 107, 108	mdslle1i 30370	. . . . . 6 ⊢ ((𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) ∧ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∨ℋ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) ⊆ (𝐴 ∨ℋ 𝐵)) → ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ↔ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ (((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵)))
112	87, 99, 110, 111	syl3anc 1373	. . . . 5 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ↔ ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ (((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵)))
113	86, 112	bitr4d 285	. . . 4 ⊢ ((((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ (((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵))) → (((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) ↔ (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))
114	113	exbiri 811	. . 3 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
115	114	a2d 29	. 2 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
116	18, 115	syld 47	1 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110   ∩ cin 3856   ⊆ wss 3857   class class class wbr 5043  (class class class)co 7202   C_ℋ cch 28982   ∨_ℋ chj 28986   𝑀_ℋ cmd 29019   𝑀_ℋ^* cdmd 29020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-inf2 9245  ax-cc 10032  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788  ax-pre-mulgt0 10789  ax-pre-sup 10790  ax-addf 10791  ax-mulf 10792  ax-hilex 29052  ax-hfvadd 29053  ax-hvcom 29054  ax-hvass 29055  ax-hv0cl 29056  ax-hvaddid 29057  ax-hfvmul 29058  ax-hvmulid 29059  ax-hvmulass 29060  ax-hvdistr1 29061  ax-hvdistr2 29062  ax-hvmul0 29063  ax-hfi 29132  ax-his1 29135  ax-his2 29136  ax-his3 29137  ax-his4 29138  ax-hcompl 29255

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-int 4850  df-iun 4896  df-iin 4897  df-br 5044  df-opab 5106  df-mpt 5125  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-se 5499  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-pred 6149  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-isom 6378  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-of 7458  df-om 7634  df-1st 7750  df-2nd 7751  df-supp 7893  df-wrecs 8036  df-recs 8097  df-rdg 8135  df-1o 8191  df-2o 8192  df-oadd 8195  df-omul 8196  df-er 8380  df-map 8499  df-pm 8500  df-ixp 8568  df-en 8616  df-dom 8617  df-sdom 8618  df-fin 8619  df-fsupp 8975  df-fi 9016  df-sup 9047  df-inf 9048  df-oi 9115  df-card 9538  df-acn 9541  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856  df-sub 11047  df-neg 11048  df-div 11473  df-nn 11814  df-2 11876  df-3 11877  df-4 11878  df-5 11879  df-6 11880  df-7 11881  df-8 11882  df-9 11883  df-n0 12074  df-z 12160  df-dec 12277  df-uz 12422  df-q 12528  df-rp 12570  df-xneg 12687  df-xadd 12688  df-xmul 12689  df-ioo 12922  df-ico 12924  df-icc 12925  df-fz 13079  df-fzo 13222  df-fl 13350  df-seq 13558  df-exp 13619  df-hash 13880  df-cj 14645  df-re 14646  df-im 14647  df-sqrt 14781  df-abs 14782  df-clim 15032  df-rlim 15033  df-sum 15233  df-struct 16686  df-ndx 16687  df-slot 16688  df-base 16690  df-sets 16691  df-ress 16692  df-plusg 16780  df-mulr 16781  df-starv 16782  df-sca 16783  df-vsca 16784  df-ip 16785  df-tset 16786  df-ple 16787  df-ds 16789  df-unif 16790  df-hom 16791  df-cco 16792  df-rest 16899  df-topn 16900  df-0g 16918  df-gsum 16919  df-topgen 16920  df-pt 16921  df-prds 16924  df-xrs 16979  df-qtop 16984  df-imas 16985  df-xps 16987  df-mre 17061  df-mrc 17062  df-acs 17064  df-mgm 18086  df-sgrp 18135  df-mnd 18146  df-submnd 18191  df-mulg 18461  df-cntz 18683  df-cmn 19144  df-psmet 20327  df-xmet 20328  df-met 20329  df-bl 20330  df-mopn 20331  df-fbas 20332  df-fg 20333  df-cnfld 20336  df-top 21763  df-topon 21780  df-topsp 21802  df-bases 21815  df-cld 21888  df-ntr 21889  df-cls 21890  df-nei 21967  df-cn 22096  df-cnp 22097  df-lm 22098  df-haus 22184  df-tx 22431  df-hmeo 22624  df-fil 22715  df-fm 22807  df-flim 22808  df-flf 22809  df-xms 23190  df-ms 23191  df-tms 23192  df-cfil 24124  df-cau 24125  df-cmet 24126  df-grpo 28546  df-gid 28547  df-ginv 28548  df-gdiv 28549  df-ablo 28598  df-vc 28612  df-nv 28645  df-va 28648  df-ba 28649  df-sm 28650  df-0v 28651  df-vs 28652  df-nmcv 28653  df-ims 28654  df-dip 28754  df-ssp 28775  df-ph 28866  df-cbn 28916  df-hnorm 29021  df-hba 29022  df-hvsub 29024  df-hlim 29025  df-hcau 29026  df-sh 29260  df-ch 29274  df-oc 29305  df-ch0 29306  df-shs 29361  df-chj 29363  df-md 30333  df-dmd 30334

This theorem is referenced by:  mdslmd1lem3  30380