Step | Hyp | Ref
| Expression |
1 | | dmdbr4 30387 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ
((𝑥 ∨ℋ
𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
2 | | chub1 29588 |
. . . . . . . . 9
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ 𝑥 ⊆ (𝑥 ∨ℋ 𝐵)) |
3 | 2 | ancoms 462 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ 𝑥 ⊆ (𝑥 ∨ℋ 𝐵)) |
4 | | ssin 4145 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ (𝑥 ∨ℋ 𝐵) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ 𝑥 ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
5 | | sstr2 3908 |
. . . . . . . . 9
⊢ (𝑥 ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
6 | 4, 5 | sylbi 220 |
. . . . . . . 8
⊢ ((𝑥 ⊆ (𝑥 ∨ℋ 𝐵) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
7 | 3, 6 | sylan 583 |
. . . . . . 7
⊢ (((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
8 | 7 | ex 416 |
. . . . . 6
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
9 | 8 | com23 86 |
. . . . 5
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
10 | 9 | ralimdva 3100 |
. . . 4
⊢ (𝐵 ∈
Cℋ → (∀𝑥 ∈ Cℋ
((𝑥 ∨ℋ
𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
11 | 10 | adantl 485 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
12 | 1, 11 | sylbid 243 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
13 | | sseq1 3926 |
. . . . . . 7
⊢ (𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ↔ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 ∨ℋ 𝐵))) |
14 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → 𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
15 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → (𝑥 ∨ℋ 𝐵) = (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵)) |
16 | 15 | ineq1d 4126 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = ((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴)) |
17 | 16 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) = (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
18 | 14, 17 | sseq12d 3934 |
. . . . . . 7
⊢ (𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → (𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
19 | 13, 18 | imbi12d 348 |
. . . . . 6
⊢ (𝑥 = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
20 | 19 | rspccv 3534 |
. . . . 5
⊢
(∀𝑥 ∈
Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
→ (((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (𝐴
∨ℋ 𝐵)
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)))) |
21 | | chjcl 29438 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑦
∨ℋ 𝐵)
∈ Cℋ ) |
22 | 21 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ (𝑦
∨ℋ 𝐵)
∈ Cℋ ) |
23 | 22 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (𝑦 ∨ℋ 𝐵) ∈ Cℋ
) |
24 | | chjcl 29438 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
∨ℋ 𝐵)
∈ Cℋ ) |
25 | 24 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ
) |
26 | | chincl 29580 |
. . . . . . . . . 10
⊢ (((𝑦 ∨ℋ 𝐵) ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∈ Cℋ ) |
27 | 23, 25, 26 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
) |
28 | | inss2 4144 |
. . . . . . . . . 10
⊢ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 ∨ℋ 𝐵) |
29 | | pm2.27 42 |
. . . . . . . . . 10
⊢ (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
→ ((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∈ Cℋ → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
30 | 28, 29 | mpii 46 |
. . . . . . . . 9
⊢ (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
→ ((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∈ Cℋ → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) → ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
31 | 27, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → ((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
→ (((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (𝐴
∨ℋ 𝐵)
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)))
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵))) |
32 | | chub2 29589 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ 𝐵 ⊆ (𝑦 ∨ℋ 𝐵)) |
33 | 32 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → 𝐵 ⊆ (𝑦 ∨ℋ 𝐵)) |
34 | | chub2 29589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ 𝐵 ⊆ (𝐴 ∨ℋ 𝐵)) |
35 | 34 | ancoms 462 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ 𝐵 ⊆ (𝐴 ∨ℋ 𝐵)) |
36 | 35 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → 𝐵 ⊆ (𝐴 ∨ℋ 𝐵)) |
37 | 33, 36 | ssind 4147 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → 𝐵 ⊆ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
38 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → 𝐵 ∈ Cℋ
) |
39 | | chlejb2 29594 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
Cℋ ∧ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
) → (𝐵 ⊆ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ↔ (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)))) |
40 | 38, 27, 39 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (𝐵 ⊆ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ↔ (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)))) |
41 | 37, 40 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) = ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
42 | 41 | ineq1d 4126 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → ((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) = (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐴)) |
43 | | inass 4134 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐴) = ((𝑦 ∨ℋ 𝐵) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐴)) |
44 | | incom 4115 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∨ℋ 𝐵) ∩ 𝐴) = (𝐴 ∩ (𝐴 ∨ℋ 𝐵)) |
45 | | chabs2 29598 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴) |
46 | 44, 45 | syl5eq 2790 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝐵)
∩ 𝐴) = 𝐴) |
47 | 46 | ineq2d 4127 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((𝑦
∨ℋ 𝐵)
∩ ((𝐴
∨ℋ 𝐵)
∩ 𝐴)) = ((𝑦 ∨ℋ 𝐵) ∩ 𝐴)) |
48 | 43, 47 | syl5eq 2790 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∩ 𝐴) = ((𝑦 ∨ℋ 𝐵) ∩ 𝐴)) |
49 | 48 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐴) = ((𝑦 ∨ℋ 𝐵) ∩ 𝐴)) |
50 | 42, 49 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → ((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) = ((𝑦 ∨ℋ 𝐵) ∩ 𝐴)) |
51 | 50 | oveq1d 7228 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) = (((𝑦 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
52 | 51 | sseq2d 3933 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑦 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
53 | 31, 52 | sylibd 242 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → ((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
→ (((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (𝐴
∨ℋ 𝐵)
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)))
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑦
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵))) |
54 | 53 | ex 416 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑦 ∈
Cℋ → ((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
→ (((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (𝐴
∨ℋ 𝐵)
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)))
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑦
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)))) |
55 | 54 | com23 86 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
∈ Cℋ → (((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((((𝑦 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) → (𝑦 ∈ Cℋ
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑦
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)))) |
56 | 20, 55 | syl5 34 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) → (𝑦 ∈ Cℋ
→ ((𝑦
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑦
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)))) |
57 | 56 | ralrimdv 3109 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) → ∀𝑦 ∈ Cℋ
((𝑦 ∨ℋ
𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑦 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
58 | | dmdbr4 30387 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑦 ∈ Cℋ
((𝑦 ∨ℋ
𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑦 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
59 | 57, 58 | sylibrd 262 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) → 𝐴 𝑀ℋ*
𝐵)) |
60 | 12, 59 | impbid 215 |
1
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |