Proof of Theorem mayetes3i
| Step | Hyp | Ref
| Expression |
| 1 | | mayetes3.a |
. . . . . . . . 9
⊢ 𝐴 ∈
Cℋ |
| 2 | | mayetes3.c |
. . . . . . . . 9
⊢ 𝐶 ∈
Cℋ |
| 3 | 1, 2 | chjcli 31476 |
. . . . . . . 8
⊢ (𝐴 ∨ℋ 𝐶) ∈
Cℋ |
| 4 | | mayetes3.f |
. . . . . . . 8
⊢ 𝐹 ∈
Cℋ |
| 5 | 3, 4 | chjcli 31476 |
. . . . . . 7
⊢ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∈
Cℋ |
| 6 | | mayetes3.r |
. . . . . . 7
⊢ 𝑅 ∈
Cℋ |
| 7 | 5, 6 | chjcomi 31487 |
. . . . . 6
⊢ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) = (𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) |
| 8 | 7 | eqimssi 4044 |
. . . . 5
⊢ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) ⊆ (𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) |
| 9 | | mayetes3.b |
. . . . . . . . . . 11
⊢ 𝐵 ∈
Cℋ |
| 10 | 1, 9 | chjcli 31476 |
. . . . . . . . . 10
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
| 11 | 10, 6 | chub1i 31488 |
. . . . . . . . 9
⊢ (𝐴 ∨ℋ 𝐵) ⊆ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝑅) |
| 12 | 1, 9, 6 | chjassi 31505 |
. . . . . . . . 9
⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝑅) = (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) |
| 13 | 11, 12 | sseqtri 4032 |
. . . . . . . 8
⊢ (𝐴 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) |
| 14 | 9, 6 | chjcli 31476 |
. . . . . . . . . 10
⊢ (𝐵 ∨ℋ 𝑅) ∈
Cℋ |
| 15 | 1, 14 | chjcli 31476 |
. . . . . . . . 9
⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∈
Cℋ |
| 16 | 15, 6 | chub2i 31489 |
. . . . . . . 8
⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ⊆ (𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) |
| 17 | 13, 16 | sstri 3993 |
. . . . . . 7
⊢ (𝐴 ∨ℋ 𝐵) ⊆ (𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) |
| 18 | | mayetes3.d |
. . . . . . . . . . 11
⊢ 𝐷 ∈
Cℋ |
| 19 | 2, 18 | chjcli 31476 |
. . . . . . . . . 10
⊢ (𝐶 ∨ℋ 𝐷) ∈
Cℋ |
| 20 | 19, 6 | chub1i 31488 |
. . . . . . . . 9
⊢ (𝐶 ∨ℋ 𝐷) ⊆ ((𝐶 ∨ℋ 𝐷) ∨ℋ 𝑅) |
| 21 | 2, 18, 6 | chjassi 31505 |
. . . . . . . . 9
⊢ ((𝐶 ∨ℋ 𝐷) ∨ℋ 𝑅) = (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)) |
| 22 | 20, 21 | sseqtri 4032 |
. . . . . . . 8
⊢ (𝐶 ∨ℋ 𝐷) ⊆ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)) |
| 23 | 18, 6 | chjcli 31476 |
. . . . . . . . . 10
⊢ (𝐷 ∨ℋ 𝑅) ∈
Cℋ |
| 24 | 2, 23 | chjcli 31476 |
. . . . . . . . 9
⊢ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)) ∈
Cℋ |
| 25 | 24, 6 | chub2i 31489 |
. . . . . . . 8
⊢ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)) ⊆ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) |
| 26 | 22, 25 | sstri 3993 |
. . . . . . 7
⊢ (𝐶 ∨ℋ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) |
| 27 | | ss2in 4245 |
. . . . . . 7
⊢ (((𝐴 ∨ℋ 𝐵) ⊆ (𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) → ((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ⊆ ((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))))) |
| 28 | 17, 26, 27 | mp2an 692 |
. . . . . 6
⊢ ((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ⊆ ((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) |
| 29 | | mayetes3.g |
. . . . . . . . . 10
⊢ 𝐺 ∈
Cℋ |
| 30 | 4, 29 | chjcli 31476 |
. . . . . . . . 9
⊢ (𝐹 ∨ℋ 𝐺) ∈
Cℋ |
| 31 | 30, 6 | chub1i 31488 |
. . . . . . . 8
⊢ (𝐹 ∨ℋ 𝐺) ⊆ ((𝐹 ∨ℋ 𝐺) ∨ℋ 𝑅) |
| 32 | 4, 29, 6 | chjassi 31505 |
. . . . . . . 8
⊢ ((𝐹 ∨ℋ 𝐺) ∨ℋ 𝑅) = (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)) |
| 33 | 31, 32 | sseqtri 4032 |
. . . . . . 7
⊢ (𝐹 ∨ℋ 𝐺) ⊆ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)) |
| 34 | 29, 6 | chjcli 31476 |
. . . . . . . . 9
⊢ (𝐺 ∨ℋ 𝑅) ∈
Cℋ |
| 35 | 4, 34 | chjcli 31476 |
. . . . . . . 8
⊢ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)) ∈
Cℋ |
| 36 | 35, 6 | chub2i 31489 |
. . . . . . 7
⊢ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)) ⊆ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))) |
| 37 | 33, 36 | sstri 3993 |
. . . . . 6
⊢ (𝐹 ∨ℋ 𝐺) ⊆ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))) |
| 38 | | ss2in 4245 |
. . . . . 6
⊢ ((((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ⊆ ((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∧ (𝐹 ∨ℋ 𝐺) ⊆ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) → (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺)) ⊆ (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) |
| 39 | 28, 37, 38 | mp2an 692 |
. . . . 5
⊢ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺)) ⊆ (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) |
| 40 | | ss2in 4245 |
. . . . 5
⊢
(((((𝐴
∨ℋ 𝐶)
∨ℋ 𝐹)
∨ℋ 𝑅)
⊆ (𝑅
∨ℋ ((𝐴
∨ℋ 𝐶)
∨ℋ 𝐹))
∧ (((𝐴
∨ℋ 𝐵)
∩ (𝐶
∨ℋ 𝐷))
∩ (𝐹
∨ℋ 𝐺))
⊆ (((𝑅
∨ℋ (𝐴
∨ℋ (𝐵
∨ℋ 𝑅)))
∩ (𝑅
∨ℋ (𝐶
∨ℋ (𝐷
∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) → ((((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) ∩ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺))) ⊆ ((𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) ∩ (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))))) |
| 41 | 8, 39, 40 | mp2an 692 |
. . . 4
⊢ ((((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) ∩ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺))) ⊆ ((𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) ∩ (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) |
| 42 | 15, 24 | chincli 31479 |
. . . . . . 7
⊢ ((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∈
Cℋ |
| 43 | 42, 35 | chincli 31479 |
. . . . . 6
⊢ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))) ∈
Cℋ |
| 44 | | mayetes3.x |
. . . . . . . . . . 11
⊢ 𝑋 = ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) |
| 45 | 44, 5 | eqeltri 2837 |
. . . . . . . . . 10
⊢ 𝑋 ∈
Cℋ |
| 46 | 45 | choccli 31326 |
. . . . . . . . 9
⊢
(⊥‘𝑋)
∈ Cℋ |
| 47 | | mayetes3.rx |
. . . . . . . . 9
⊢ 𝑅 ⊆ (⊥‘𝑋) |
| 48 | 6, 46, 47 | lecmii 31622 |
. . . . . . . 8
⊢ 𝑅 𝐶ℋ
(⊥‘𝑋) |
| 49 | 6, 45 | cmcm2i 31612 |
. . . . . . . 8
⊢ (𝑅 𝐶ℋ
𝑋 ↔ 𝑅 𝐶ℋ
(⊥‘𝑋)) |
| 50 | 48, 49 | mpbir 231 |
. . . . . . 7
⊢ 𝑅 𝐶ℋ
𝑋 |
| 51 | 50, 44 | breqtri 5168 |
. . . . . 6
⊢ 𝑅 𝐶ℋ
((𝐴 ∨ℋ
𝐶) ∨ℋ
𝐹) |
| 52 | 6, 9 | chub2i 31489 |
. . . . . . . . . 10
⊢ 𝑅 ⊆ (𝐵 ∨ℋ 𝑅) |
| 53 | 14, 1 | chub2i 31489 |
. . . . . . . . . 10
⊢ (𝐵 ∨ℋ 𝑅) ⊆ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) |
| 54 | 52, 53 | sstri 3993 |
. . . . . . . . 9
⊢ 𝑅 ⊆ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) |
| 55 | 6, 15, 54 | lecmii 31622 |
. . . . . . . 8
⊢ 𝑅 𝐶ℋ
(𝐴 ∨ℋ
(𝐵 ∨ℋ
𝑅)) |
| 56 | 6, 18 | chub2i 31489 |
. . . . . . . . . 10
⊢ 𝑅 ⊆ (𝐷 ∨ℋ 𝑅) |
| 57 | 23, 2 | chub2i 31489 |
. . . . . . . . . 10
⊢ (𝐷 ∨ℋ 𝑅) ⊆ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)) |
| 58 | 56, 57 | sstri 3993 |
. . . . . . . . 9
⊢ 𝑅 ⊆ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)) |
| 59 | 6, 24, 58 | lecmii 31622 |
. . . . . . . 8
⊢ 𝑅 𝐶ℋ
(𝐶 ∨ℋ
(𝐷 ∨ℋ
𝑅)) |
| 60 | 6, 15, 24, 55, 59 | cm2mi 31645 |
. . . . . . 7
⊢ 𝑅 𝐶ℋ
((𝐴 ∨ℋ
(𝐵 ∨ℋ
𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) |
| 61 | 6, 29 | chub2i 31489 |
. . . . . . . . 9
⊢ 𝑅 ⊆ (𝐺 ∨ℋ 𝑅) |
| 62 | 34, 4 | chub2i 31489 |
. . . . . . . . 9
⊢ (𝐺 ∨ℋ 𝑅) ⊆ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)) |
| 63 | 61, 62 | sstri 3993 |
. . . . . . . 8
⊢ 𝑅 ⊆ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)) |
| 64 | 6, 35, 63 | lecmii 31622 |
. . . . . . 7
⊢ 𝑅 𝐶ℋ
(𝐹 ∨ℋ
(𝐺 ∨ℋ
𝑅)) |
| 65 | 6, 42, 35, 60, 64 | cm2mi 31645 |
. . . . . 6
⊢ 𝑅 𝐶ℋ
(((𝐴 ∨ℋ
(𝐵 ∨ℋ
𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))) |
| 66 | 6, 5, 43, 51, 65 | fh3i 31642 |
. . . . 5
⊢ (𝑅 ∨ℋ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) = ((𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) ∩ (𝑅 ∨ℋ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) |
| 67 | 6, 42, 35, 60, 64 | fh3i 31642 |
. . . . . . 7
⊢ (𝑅 ∨ℋ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) = ((𝑅 ∨ℋ ((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) |
| 68 | 6, 15, 24, 55, 59 | fh3i 31642 |
. . . . . . . 8
⊢ (𝑅 ∨ℋ ((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) = ((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) |
| 69 | 68 | ineq1i 4216 |
. . . . . . 7
⊢ ((𝑅 ∨ℋ ((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) = (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) |
| 70 | 67, 69 | eqtri 2765 |
. . . . . 6
⊢ (𝑅 ∨ℋ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) = (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) |
| 71 | 70 | ineq2i 4217 |
. . . . 5
⊢ ((𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) ∩ (𝑅 ∨ℋ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) = ((𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) ∩ (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) |
| 72 | 66, 71 | eqtr2i 2766 |
. . . 4
⊢ ((𝑅 ∨ℋ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹)) ∩ (((𝑅 ∨ℋ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅))) ∩ (𝑅 ∨ℋ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅)))) ∩ (𝑅 ∨ℋ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) = (𝑅 ∨ℋ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) |
| 73 | 41, 72 | sseqtri 4032 |
. . 3
⊢ ((((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) ∩ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺))) ⊆ (𝑅 ∨ℋ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) |
| 74 | 9, 18 | chjcli 31476 |
. . . . . 6
⊢ (𝐵 ∨ℋ 𝐷) ∈
Cℋ |
| 75 | 74, 29 | chjcli 31476 |
. . . . 5
⊢ ((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∈
Cℋ |
| 76 | 6, 75 | chub2i 31489 |
. . . 4
⊢ 𝑅 ⊆ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) |
| 77 | | mayetes3.ac |
. . . . 5
⊢ 𝐴 ⊆ (⊥‘𝐶) |
| 78 | | mayetes3.af |
. . . . 5
⊢ 𝐴 ⊆ (⊥‘𝐹) |
| 79 | | mayetes3.cf |
. . . . 5
⊢ 𝐶 ⊆ (⊥‘𝐹) |
| 80 | | mayetes3.ab |
. . . . . . 7
⊢ 𝐴 ⊆ (⊥‘𝐵) |
| 81 | 1, 2 | chub1i 31488 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐶) |
| 82 | 3, 4 | chub1i 31488 |
. . . . . . . . . . . 12
⊢ (𝐴 ∨ℋ 𝐶) ⊆ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) |
| 83 | 82, 44 | sseqtrri 4033 |
. . . . . . . . . . 11
⊢ (𝐴 ∨ℋ 𝐶) ⊆ 𝑋 |
| 84 | 81, 83 | sstri 3993 |
. . . . . . . . . 10
⊢ 𝐴 ⊆ 𝑋 |
| 85 | 1, 45 | chsscon3i 31480 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝑋 ↔ (⊥‘𝑋) ⊆ (⊥‘𝐴)) |
| 86 | 84, 85 | mpbi 230 |
. . . . . . . . 9
⊢
(⊥‘𝑋)
⊆ (⊥‘𝐴) |
| 87 | 47, 86 | sstri 3993 |
. . . . . . . 8
⊢ 𝑅 ⊆ (⊥‘𝐴) |
| 88 | 6, 1 | chsscon2i 31482 |
. . . . . . . 8
⊢ (𝑅 ⊆ (⊥‘𝐴) ↔ 𝐴 ⊆ (⊥‘𝑅)) |
| 89 | 87, 88 | mpbi 230 |
. . . . . . 7
⊢ 𝐴 ⊆ (⊥‘𝑅) |
| 90 | 80, 89 | ssini 4240 |
. . . . . 6
⊢ 𝐴 ⊆ ((⊥‘𝐵) ∩ (⊥‘𝑅)) |
| 91 | 9, 6 | chdmj1i 31500 |
. . . . . 6
⊢
(⊥‘(𝐵
∨ℋ 𝑅))
= ((⊥‘𝐵) ∩
(⊥‘𝑅)) |
| 92 | 90, 91 | sseqtrri 4033 |
. . . . 5
⊢ 𝐴 ⊆ (⊥‘(𝐵 ∨ℋ 𝑅)) |
| 93 | | mayetes3.cd |
. . . . . . 7
⊢ 𝐶 ⊆ (⊥‘𝐷) |
| 94 | 2, 1 | chub2i 31489 |
. . . . . . . . . . 11
⊢ 𝐶 ⊆ (𝐴 ∨ℋ 𝐶) |
| 95 | 94, 83 | sstri 3993 |
. . . . . . . . . 10
⊢ 𝐶 ⊆ 𝑋 |
| 96 | 2, 45 | chsscon3i 31480 |
. . . . . . . . . 10
⊢ (𝐶 ⊆ 𝑋 ↔ (⊥‘𝑋) ⊆ (⊥‘𝐶)) |
| 97 | 95, 96 | mpbi 230 |
. . . . . . . . 9
⊢
(⊥‘𝑋)
⊆ (⊥‘𝐶) |
| 98 | 47, 97 | sstri 3993 |
. . . . . . . 8
⊢ 𝑅 ⊆ (⊥‘𝐶) |
| 99 | 6, 2 | chsscon2i 31482 |
. . . . . . . 8
⊢ (𝑅 ⊆ (⊥‘𝐶) ↔ 𝐶 ⊆ (⊥‘𝑅)) |
| 100 | 98, 99 | mpbi 230 |
. . . . . . 7
⊢ 𝐶 ⊆ (⊥‘𝑅) |
| 101 | 93, 100 | ssini 4240 |
. . . . . 6
⊢ 𝐶 ⊆ ((⊥‘𝐷) ∩ (⊥‘𝑅)) |
| 102 | 18, 6 | chdmj1i 31500 |
. . . . . 6
⊢
(⊥‘(𝐷
∨ℋ 𝑅))
= ((⊥‘𝐷) ∩
(⊥‘𝑅)) |
| 103 | 101, 102 | sseqtrri 4033 |
. . . . 5
⊢ 𝐶 ⊆ (⊥‘(𝐷 ∨ℋ 𝑅)) |
| 104 | | mayetes3.fg |
. . . . . . 7
⊢ 𝐹 ⊆ (⊥‘𝐺) |
| 105 | 4, 3 | chub2i 31489 |
. . . . . . . . . . 11
⊢ 𝐹 ⊆ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) |
| 106 | 105, 44 | sseqtrri 4033 |
. . . . . . . . . 10
⊢ 𝐹 ⊆ 𝑋 |
| 107 | 4, 45 | chsscon3i 31480 |
. . . . . . . . . 10
⊢ (𝐹 ⊆ 𝑋 ↔ (⊥‘𝑋) ⊆ (⊥‘𝐹)) |
| 108 | 106, 107 | mpbi 230 |
. . . . . . . . 9
⊢
(⊥‘𝑋)
⊆ (⊥‘𝐹) |
| 109 | 47, 108 | sstri 3993 |
. . . . . . . 8
⊢ 𝑅 ⊆ (⊥‘𝐹) |
| 110 | 6, 4 | chsscon2i 31482 |
. . . . . . . 8
⊢ (𝑅 ⊆ (⊥‘𝐹) ↔ 𝐹 ⊆ (⊥‘𝑅)) |
| 111 | 109, 110 | mpbi 230 |
. . . . . . 7
⊢ 𝐹 ⊆ (⊥‘𝑅) |
| 112 | 104, 111 | ssini 4240 |
. . . . . 6
⊢ 𝐹 ⊆ ((⊥‘𝐺) ∩ (⊥‘𝑅)) |
| 113 | 29, 6 | chdmj1i 31500 |
. . . . . 6
⊢
(⊥‘(𝐺
∨ℋ 𝑅))
= ((⊥‘𝐺) ∩
(⊥‘𝑅)) |
| 114 | 112, 113 | sseqtrri 4033 |
. . . . 5
⊢ 𝐹 ⊆ (⊥‘(𝐺 ∨ℋ 𝑅)) |
| 115 | | eqid 2737 |
. . . . 5
⊢ ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) = ((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) |
| 116 | | eqid 2737 |
. . . . 5
⊢ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))) = (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))) |
| 117 | 74, 29, 6 | chjjdiri 31543 |
. . . . . 6
⊢ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) = (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝑅) ∨ℋ (𝐺 ∨ℋ 𝑅)) |
| 118 | 9, 18, 6 | chjjdiri 31543 |
. . . . . . 7
⊢ ((𝐵 ∨ℋ 𝐷) ∨ℋ 𝑅) = ((𝐵 ∨ℋ 𝑅) ∨ℋ (𝐷 ∨ℋ 𝑅)) |
| 119 | 118 | oveq1i 7441 |
. . . . . 6
⊢ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝑅) ∨ℋ (𝐺 ∨ℋ 𝑅)) = (((𝐵 ∨ℋ 𝑅) ∨ℋ (𝐷 ∨ℋ 𝑅)) ∨ℋ (𝐺 ∨ℋ 𝑅)) |
| 120 | 117, 119 | eqtri 2765 |
. . . . 5
⊢ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) = (((𝐵 ∨ℋ 𝑅) ∨ℋ (𝐷 ∨ℋ 𝑅)) ∨ℋ (𝐺 ∨ℋ 𝑅)) |
| 121 | 1, 14, 2, 23, 4, 34, 77, 78, 79, 92, 103, 114, 115, 116, 120 | mayete3i 31747 |
. . . 4
⊢ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) ⊆ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) |
| 122 | 5, 43 | chincli 31479 |
. . . . 5
⊢ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) ∈
Cℋ |
| 123 | 75, 6 | chjcli 31476 |
. . . . 5
⊢ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) ∈
Cℋ |
| 124 | 6, 122, 123 | chlubii 31491 |
. . . 4
⊢ ((𝑅 ⊆ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) ∧ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅)))) ⊆ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅)) → (𝑅 ∨ℋ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) ⊆ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅)) |
| 125 | 76, 121, 124 | mp2an 692 |
. . 3
⊢ (𝑅 ∨ℋ (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∩ (((𝐴 ∨ℋ (𝐵 ∨ℋ 𝑅)) ∩ (𝐶 ∨ℋ (𝐷 ∨ℋ 𝑅))) ∩ (𝐹 ∨ℋ (𝐺 ∨ℋ 𝑅))))) ⊆ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) |
| 126 | 73, 125 | sstri 3993 |
. 2
⊢ ((((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) ∩ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺))) ⊆ (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) |
| 127 | 44 | oveq1i 7441 |
. . 3
⊢ (𝑋 ∨ℋ 𝑅) = (((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) |
| 128 | | mayetes3.y |
. . 3
⊢ 𝑌 = (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺)) |
| 129 | 127, 128 | ineq12i 4218 |
. 2
⊢ ((𝑋 ∨ℋ 𝑅) ∩ 𝑌) = ((((𝐴 ∨ℋ 𝐶) ∨ℋ 𝐹) ∨ℋ 𝑅) ∩ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ (𝐹 ∨ℋ 𝐺))) |
| 130 | | mayetes3.z |
. . 3
⊢ 𝑍 = ((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) |
| 131 | 130 | oveq1i 7441 |
. 2
⊢ (𝑍 ∨ℋ 𝑅) = (((𝐵 ∨ℋ 𝐷) ∨ℋ 𝐺) ∨ℋ 𝑅) |
| 132 | 126, 129,
131 | 3sstr4i 4035 |
1
⊢ ((𝑋 ∨ℋ 𝑅) ∩ 𝑌) ⊆ (𝑍 ∨ℋ 𝑅) |