Step | Hyp | Ref
| Expression |
1 | | cdmd 30251 |
. 2
class
𝑀ℋ* |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
4 | | cch 30213 |
. . . . . 6
class
Cℋ |
5 | 3, 4 | wcel 2107 |
. . . . 5
wff 𝑥 ∈
Cℋ |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1541 |
. . . . . 6
class 𝑦 |
8 | 7, 4 | wcel 2107 |
. . . . 5
wff 𝑦 ∈
Cℋ |
9 | 5, 8 | wa 397 |
. . . 4
wff (𝑥 ∈
Cℋ ∧ 𝑦 ∈ Cℋ
) |
10 | | vz |
. . . . . . . 8
setvar 𝑧 |
11 | 10 | cv 1541 |
. . . . . . 7
class 𝑧 |
12 | 7, 11 | wss 3949 |
. . . . . 6
wff 𝑦 ⊆ 𝑧 |
13 | 11, 3 | cin 3948 |
. . . . . . . 8
class (𝑧 ∩ 𝑥) |
14 | | chj 30217 |
. . . . . . . 8
class
∨ℋ |
15 | 13, 7, 14 | co 7409 |
. . . . . . 7
class ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) |
16 | 3, 7, 14 | co 7409 |
. . . . . . . 8
class (𝑥 ∨ℋ 𝑦) |
17 | 11, 16 | cin 3948 |
. . . . . . 7
class (𝑧 ∩ (𝑥 ∨ℋ 𝑦)) |
18 | 15, 17 | wceq 1542 |
. . . . . 6
wff ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦)) |
19 | 12, 18 | wi 4 |
. . . . 5
wff (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))) |
20 | 19, 10, 4 | wral 3062 |
. . . 4
wff
∀𝑧 ∈
Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))) |
21 | 9, 20 | wa 397 |
. . 3
wff ((𝑥 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ ∀𝑧 ∈
Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦)))) |
22 | 21, 2, 6 | copab 5211 |
. 2
class
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ ∀𝑧 ∈
Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))} |
23 | 1, 22 | wceq 1542 |
1
wff
𝑀ℋ* = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ) ∧ ∀𝑧 ∈ Cℋ
(𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))} |