Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π΅ β πΎ β V) |
2 | | psubclset.c |
. . 3
β’ πΆ = (PSubClβπΎ) |
3 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
4 | | psubclset.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (Atomsβπ) = π΄) |
6 | 5 | sseq2d 3977 |
. . . . . 6
β’ (π = πΎ β (π β (Atomsβπ) β π β π΄)) |
7 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β
(β₯πβπ) = (β₯πβπΎ)) |
8 | | psubclset.p |
. . . . . . . . 9
β’ β₯ =
(β₯πβπΎ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΎ β
(β₯πβπ) = β₯ ) |
10 | 9 | fveq1d 6845 |
. . . . . . . 8
β’ (π = πΎ β
((β₯πβπ)βπ ) = ( β₯ βπ )) |
11 | 9, 10 | fveq12d 6850 |
. . . . . . 7
β’ (π = πΎ β
((β₯πβπ)β((β₯πβπ)βπ )) = ( β₯ β( β₯
βπ ))) |
12 | 11 | eqeq1d 2739 |
. . . . . 6
β’ (π = πΎ β
(((β₯πβπ)β((β₯πβπ)βπ )) = π β ( β₯ β( β₯
βπ )) = π )) |
13 | 6, 12 | anbi12d 632 |
. . . . 5
β’ (π = πΎ β ((π β (Atomsβπ) β§
((β₯πβπ)β((β₯πβπ)βπ )) = π ) β (π β π΄ β§ ( β₯ β( β₯
βπ )) = π ))) |
14 | 13 | abbidv 2806 |
. . . 4
β’ (π = πΎ β {π β£ (π β (Atomsβπ) β§
((β₯πβπ)β((β₯πβπ)βπ )) = π )} = {π β£ (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )}) |
15 | | df-psubclN 38401 |
. . . 4
β’ PSubCl =
(π β V β¦ {π β£ (π β (Atomsβπ) β§
((β₯πβπ)β((β₯πβπ)βπ )) = π )}) |
16 | 4 | fvexi 6857 |
. . . . . 6
β’ π΄ β V |
17 | 16 | pwex 5336 |
. . . . 5
β’ π«
π΄ β V |
18 | | velpw 4566 |
. . . . . . . 8
β’ (π β π« π΄ β π β π΄) |
19 | 18 | anbi1i 625 |
. . . . . . 7
β’ ((π β π« π΄ β§ ( β₯ β( β₯
βπ )) = π ) β (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )) |
20 | 19 | abbii 2807 |
. . . . . 6
β’ {π β£ (π β π« π΄ β§ ( β₯ β( β₯
βπ )) = π )} = {π β£ (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )} |
21 | | ssab2 4037 |
. . . . . 6
β’ {π β£ (π β π« π΄ β§ ( β₯ β( β₯
βπ )) = π )} β π« π΄ |
22 | 20, 21 | eqsstrri 3980 |
. . . . 5
β’ {π β£ (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )} β π« π΄ |
23 | 17, 22 | ssexi 5280 |
. . . 4
β’ {π β£ (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )} β V |
24 | 14, 15, 23 | fvmpt 6949 |
. . 3
β’ (πΎ β V β
(PSubClβπΎ) = {π β£ (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )}) |
25 | 2, 24 | eqtrid 2789 |
. 2
β’ (πΎ β V β πΆ = {π β£ (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )}) |
26 | 1, 25 | syl 17 |
1
β’ (πΎ β π΅ β πΆ = {π β£ (π β π΄ β§ ( β₯ β( β₯
βπ )) = π )}) |