Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π΄ β πΎ β V) |
2 | | cmtfval.c |
. . 3
β’ πΆ = (cmβπΎ) |
3 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | cmtfval.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | 5 | eleq2d 2824 |
. . . . . 6
β’ (π = πΎ β (π₯ β (Baseβπ) β π₯ β π΅)) |
7 | 5 | eleq2d 2824 |
. . . . . 6
β’ (π = πΎ β (π¦ β (Baseβπ) β π¦ β π΅)) |
8 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
9 | | cmtfval.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΎ β (joinβπ) = β¨ ) |
11 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = πΎ β (meetβπ) = (meetβπΎ)) |
12 | | cmtfval.m |
. . . . . . . . . 10
β’ β§ =
(meetβπΎ) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π = πΎ β (meetβπ) = β§ ) |
14 | 13 | oveqd 7375 |
. . . . . . . 8
β’ (π = πΎ β (π₯(meetβπ)π¦) = (π₯ β§ π¦)) |
15 | | eqidd 2738 |
. . . . . . . . 9
β’ (π = πΎ β π₯ = π₯) |
16 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = πΎ β (ocβπ) = (ocβπΎ)) |
17 | | cmtfval.o |
. . . . . . . . . . 11
β’ β₯ =
(ocβπΎ) |
18 | 16, 17 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = πΎ β (ocβπ) = β₯ ) |
19 | 18 | fveq1d 6845 |
. . . . . . . . 9
β’ (π = πΎ β ((ocβπ)βπ¦) = ( β₯ βπ¦)) |
20 | 13, 15, 19 | oveq123d 7379 |
. . . . . . . 8
β’ (π = πΎ β (π₯(meetβπ)((ocβπ)βπ¦)) = (π₯ β§ ( β₯ βπ¦))) |
21 | 10, 14, 20 | oveq123d 7379 |
. . . . . . 7
β’ (π = πΎ β ((π₯(meetβπ)π¦)(joinβπ)(π₯(meetβπ)((ocβπ)βπ¦))) = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦)))) |
22 | 21 | eqeq2d 2748 |
. . . . . 6
β’ (π = πΎ β (π₯ = ((π₯(meetβπ)π¦)(joinβπ)(π₯(meetβπ)((ocβπ)βπ¦))) β π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))) |
23 | 6, 7, 22 | 3anbi123d 1437 |
. . . . 5
β’ (π = πΎ β ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π₯ = ((π₯(meetβπ)π¦)(joinβπ)(π₯(meetβπ)((ocβπ)βπ¦)))) β (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦)))))) |
24 | 23 | opabbidv 5172 |
. . . 4
β’ (π = πΎ β {β¨π₯, π¦β© β£ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π₯ = ((π₯(meetβπ)π¦)(joinβπ)(π₯(meetβπ)((ocβπ)βπ¦))))} = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))}) |
25 | | df-cmtN 37642 |
. . . 4
β’ cm =
(π β V β¦
{β¨π₯, π¦β© β£ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π₯ = ((π₯(meetβπ)π¦)(joinβπ)(π₯(meetβπ)((ocβπ)βπ¦))))}) |
26 | | df-3an 1090 |
. . . . . 6
β’ ((π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦)))) β ((π₯ β π΅ β§ π¦ β π΅) β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))) |
27 | 26 | opabbii 5173 |
. . . . 5
β’
{β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))} = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))} |
28 | 4 | fvexi 6857 |
. . . . . . 7
β’ π΅ β V |
29 | 28, 28 | xpex 7688 |
. . . . . 6
β’ (π΅ Γ π΅) β V |
30 | | opabssxp 5725 |
. . . . . 6
β’
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))} β (π΅ Γ π΅) |
31 | 29, 30 | ssexi 5280 |
. . . . 5
β’
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))} β V |
32 | 27, 31 | eqeltri 2834 |
. . . 4
β’
{β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))} β V |
33 | 24, 25, 32 | fvmpt 6949 |
. . 3
β’ (πΎ β V β (cmβπΎ) = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))}) |
34 | 2, 33 | eqtrid 2789 |
. 2
β’ (πΎ β V β πΆ = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))}) |
35 | 1, 34 | syl 17 |
1
β’ (πΎ β π΄ β πΆ = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ π¦ β π΅ β§ π₯ = ((π₯ β§ π¦) β¨ (π₯ β§ ( β₯ βπ¦))))}) |