Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝐾 ∈ V) |
2 | | psubclset.c |
. . 3
⊢ 𝐶 = (PSubCl‘𝐾) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
4 | | psubclset.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
6 | 5 | sseq2d 3596 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑠 ⊆ (Atoms‘𝑘) ↔ 𝑠 ⊆ 𝐴)) |
7 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 →
(⊥𝑃‘𝑘) = (⊥𝑃‘𝐾)) |
8 | | psubclset.p |
. . . . . . . . 9
⊢ ⊥ =
(⊥𝑃‘𝐾) |
9 | 7, 8 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 →
(⊥𝑃‘𝑘) = ⊥ ) |
10 | 9 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 →
((⊥𝑃‘𝑘)‘𝑠) = ( ⊥ ‘𝑠)) |
11 | 9, 10 | fveq12d 6109 |
. . . . . . 7
⊢ (𝑘 = 𝐾 →
((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = ( ⊥ ‘( ⊥
‘𝑠))) |
12 | 11 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑘 = 𝐾 →
(((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠 ↔ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)) |
13 | 6, 12 | anbi12d 743 |
. . . . 5
⊢ (𝑘 = 𝐾 → ((𝑠 ⊆ (Atoms‘𝑘) ∧
((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠) ↔ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠))) |
14 | 13 | abbidv 2728 |
. . . 4
⊢ (𝑘 = 𝐾 → {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧
((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)} = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)}) |
15 | | df-psubclN 34239 |
. . . 4
⊢ PSubCl =
(𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧
((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)}) |
16 | | fvex 6113 |
. . . . . . 7
⊢
(Atoms‘𝐾)
∈ V |
17 | 4, 16 | eqeltri 2684 |
. . . . . 6
⊢ 𝐴 ∈ V |
18 | 17 | pwex 4774 |
. . . . 5
⊢ 𝒫
𝐴 ∈ V |
19 | | selpw 4115 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝒫 𝐴 ↔ 𝑠 ⊆ 𝐴) |
20 | 19 | anbi1i 727 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝒫 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠) ↔ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)) |
21 | 20 | abbii 2726 |
. . . . . 6
⊢ {𝑠 ∣ (𝑠 ∈ 𝒫 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)} = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)} |
22 | | ssab2 3649 |
. . . . . 6
⊢ {𝑠 ∣ (𝑠 ∈ 𝒫 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)} ⊆ 𝒫 𝐴 |
23 | 21, 22 | eqsstr3i 3599 |
. . . . 5
⊢ {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)} ⊆ 𝒫 𝐴 |
24 | 18, 23 | ssexi 4731 |
. . . 4
⊢ {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)} ∈ V |
25 | 14, 15, 24 | fvmpt 6191 |
. . 3
⊢ (𝐾 ∈ V →
(PSubCl‘𝐾) = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)}) |
26 | 2, 25 | syl5eq 2656 |
. 2
⊢ (𝐾 ∈ V → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)}) |
27 | 1, 26 | syl 17 |
1
⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥
‘𝑠)) = 𝑠)}) |