Proof of Theorem mdslj1i
Step | Hyp | Ref
| Expression |
1 | | ssin 3797 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ↔ 𝐴 ⊆ (𝐶 ∩ 𝐷)) |
2 | 1 | bicomi 213 |
. . . 4
⊢ (𝐴 ⊆ (𝐶 ∩ 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷)) |
3 | | mdslle1.3 |
. . . . . 6
⊢ 𝐶 ∈
Cℋ |
4 | | mdslle1.4 |
. . . . . 6
⊢ 𝐷 ∈
Cℋ |
5 | | mdslle1.1 |
. . . . . . 7
⊢ 𝐴 ∈
Cℋ |
6 | | mdslle1.2 |
. . . . . . 7
⊢ 𝐵 ∈
Cℋ |
7 | 5, 6 | chjcli 27700 |
. . . . . 6
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
8 | 3, 4, 7 | chlubi 27714 |
. . . . 5
⊢ ((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
9 | 8 | bicomi 213 |
. . . 4
⊢ ((𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵) ↔ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) |
10 | 2, 9 | anbi12i 729 |
. . 3
⊢ ((𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) ↔ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) |
11 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) → 𝐵 𝑀ℋ*
𝐴) |
12 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) → 𝐴 ⊆ 𝐶) |
13 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝐶 ⊆ (𝐴 ∨ℋ 𝐵)) |
14 | 5, 6, 3 | 3pm3.2i 1232 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) |
15 | | dmdsl3 28558 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝑀ℋ*
𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∩ 𝐵) ∨ℋ 𝐴) = 𝐶) |
16 | 14, 15 | mpan 702 |
. . . . . . . . . 10
⊢ ((𝐵
𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝐶 ∩ 𝐵) ∨ℋ 𝐴) = 𝐶) |
17 | 11, 12, 13, 16 | syl3an 1360 |
. . . . . . . . 9
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∩ 𝐵) ∨ℋ 𝐴) = 𝐶) |
18 | 3, 6 | chincli 27703 |
. . . . . . . . . . 11
⊢ (𝐶 ∩ 𝐵) ∈
Cℋ |
19 | 4, 6 | chincli 27703 |
. . . . . . . . . . 11
⊢ (𝐷 ∩ 𝐵) ∈
Cℋ |
20 | 18, 19 | chub1i 27712 |
. . . . . . . . . 10
⊢ (𝐶 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) |
21 | 18, 19 | chjcli 27700 |
. . . . . . . . . . 11
⊢ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∈
Cℋ |
22 | 18, 21, 5 | chlej1i 27716 |
. . . . . . . . . 10
⊢ ((𝐶 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) → ((𝐶 ∩ 𝐵) ∨ℋ 𝐴) ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
23 | 20, 22 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∩ 𝐵) ∨ℋ 𝐴) ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
24 | 17, 23 | eqsstr3d 3603 |
. . . . . . . 8
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝐶 ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
25 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) → 𝐴 ⊆ 𝐷) |
26 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) |
27 | 5, 6, 4 | 3pm3.2i 1232 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐷 ∈
Cℋ ) |
28 | | dmdsl3 28558 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐷 ∈
Cℋ ) ∧ (𝐵 𝑀ℋ*
𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) = 𝐷) |
29 | 27, 28 | mpan 702 |
. . . . . . . . . 10
⊢ ((𝐵
𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) = 𝐷) |
30 | 11, 25, 26, 29 | syl3an 1360 |
. . . . . . . . 9
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) = 𝐷) |
31 | 19, 18 | chub2i 27713 |
. . . . . . . . . 10
⊢ (𝐷 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) |
32 | 19, 21, 5 | chlej1i 27716 |
. . . . . . . . . 10
⊢ ((𝐷 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
33 | 31, 32 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐷 ∩ 𝐵) ∨ℋ 𝐴) ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
34 | 30, 33 | eqsstr3d 3603 |
. . . . . . . 8
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝐷 ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
35 | 24, 34 | jca 553 |
. . . . . . 7
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∧ 𝐷 ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴))) |
36 | 21, 5 | chjcli 27700 |
. . . . . . . 8
⊢ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∈
Cℋ |
37 | 3, 4, 36 | chlubi 27714 |
. . . . . . 7
⊢ ((𝐶 ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∧ 𝐷 ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) ↔ (𝐶 ∨ℋ 𝐷) ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
38 | 35, 37 | sylib 207 |
. . . . . 6
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 ∨ℋ 𝐷) ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴)) |
39 | | ssrin 3800 |
. . . . . 6
⊢ ((𝐶 ∨ℋ 𝐷) ⊆ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) ⊆ ((((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∩ 𝐵)) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) ⊆ ((((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∩ 𝐵)) |
41 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) → 𝐴 𝑀ℋ 𝐵) |
42 | | ssrin 3800 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐵)) |
43 | 42, 20 | syl6ss 3580 |
. . . . . . 7
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
44 | 43 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) → (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
45 | | inss2 3796 |
. . . . . . . 8
⊢ (𝐶 ∩ 𝐵) ⊆ 𝐵 |
46 | | inss2 3796 |
. . . . . . . 8
⊢ (𝐷 ∩ 𝐵) ⊆ 𝐵 |
47 | 18, 19, 6 | chlubi 27714 |
. . . . . . . . 9
⊢ (((𝐶 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐷 ∩ 𝐵) ⊆ 𝐵) ↔ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ 𝐵) |
48 | 47 | bicomi 213 |
. . . . . . . 8
⊢ (((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ 𝐵 ↔ ((𝐶 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐷 ∩ 𝐵) ⊆ 𝐵)) |
49 | 45, 46, 48 | mpbir2an 957 |
. . . . . . 7
⊢ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ 𝐵 |
50 | 49 | a1i 11 |
. . . . . 6
⊢ ((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ 𝐵) |
51 | 5, 6, 21 | 3pm3.2i 1232 |
. . . . . . 7
⊢ (𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∈ Cℋ
) |
52 | | mdsl3 28559 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∈ Cℋ
) ∧ (𝐴
𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∧ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ 𝐵)) → ((((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
53 | 51, 52 | mpan 702 |
. . . . . 6
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∧ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ 𝐵) → ((((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
54 | 41, 44, 50, 53 | syl3an 1360 |
. . . . 5
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ∨ℋ 𝐴) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
55 | 40, 54 | sseqtrd 3604 |
. . . 4
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
56 | 55 | 3expb 1258 |
. . 3
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
57 | 10, 56 | sylan2b 491 |
. 2
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) ⊆ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |
58 | 3, 4, 6 | lediri 27780 |
. . 3
⊢ ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) |
59 | 58 | a1i 11 |
. 2
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)) ⊆ ((𝐶 ∨ℋ 𝐷) ∩ 𝐵)) |
60 | 57, 59 | eqssd 3585 |
1
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) |