Step | Hyp | Ref
| Expression |
1 | | mclsval.c |
. . 3
β’ πΆ = (mClsβπ) |
2 | | mclsval.1 |
. . . 4
β’ (π β π β mFS) |
3 | | elex 3461 |
. . . 4
β’ (π β mFS β π β V) |
4 | | fveq2 6839 |
. . . . . . . 8
β’ (π‘ = π β (mDVβπ‘) = (mDVβπ)) |
5 | | mclsval.d |
. . . . . . . 8
β’ π· = (mDVβπ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . . . 7
β’ (π‘ = π β (mDVβπ‘) = π·) |
7 | 6 | pweqd 4575 |
. . . . . 6
β’ (π‘ = π β π« (mDVβπ‘) = π« π·) |
8 | | fveq2 6839 |
. . . . . . . 8
β’ (π‘ = π β (mExβπ‘) = (mExβπ)) |
9 | | mclsval.e |
. . . . . . . 8
β’ πΈ = (mExβπ) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . . 7
β’ (π‘ = π β (mExβπ‘) = πΈ) |
11 | 10 | pweqd 4575 |
. . . . . 6
β’ (π‘ = π β π« (mExβπ‘) = π« πΈ) |
12 | | fveq2 6839 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (mVHβπ‘) = (mVHβπ)) |
13 | | mclsval.h |
. . . . . . . . . . . . 13
β’ π» = (mVHβπ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ (π‘ = π β (mVHβπ‘) = π») |
15 | 14 | rneqd 5891 |
. . . . . . . . . . 11
β’ (π‘ = π β ran (mVHβπ‘) = ran π») |
16 | 15 | uneq2d 4121 |
. . . . . . . . . 10
β’ (π‘ = π β (β βͺ ran (mVHβπ‘)) = (β βͺ ran π»)) |
17 | 16 | sseq1d 3973 |
. . . . . . . . 9
β’ (π‘ = π β ((β βͺ ran (mVHβπ‘)) β π β (β βͺ ran π») β π)) |
18 | | fveq2 6839 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β (mAxβπ‘) = (mAxβπ)) |
19 | | mclsval.a |
. . . . . . . . . . . . . 14
β’ π΄ = (mAxβπ) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (mAxβπ‘) = π΄) |
21 | 20 | eleq2d 2823 |
. . . . . . . . . . . 12
β’ (π‘ = π β (β¨π, π, πβ© β (mAxβπ‘) β β¨π, π, πβ© β π΄)) |
22 | | fveq2 6839 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β (mSubstβπ‘) = (mSubstβπ)) |
23 | | mclsval.s |
. . . . . . . . . . . . . . 15
β’ π = (mSubstβπ) |
24 | 22, 23 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β (mSubstβπ‘) = π) |
25 | 24 | rneqd 5891 |
. . . . . . . . . . . . 13
β’ (π‘ = π β ran (mSubstβπ‘) = ran π) |
26 | 15 | uneq2d 4121 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = π β (π βͺ ran (mVHβπ‘)) = (π βͺ ran π»)) |
27 | 26 | imaeq2d 6011 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = π β (π β (π βͺ ran (mVHβπ‘))) = (π β (π βͺ ran π»))) |
28 | 27 | sseq1d 3973 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β ((π β (π βͺ ran (mVHβπ‘))) β π β (π β (π βͺ ran π»)) β π)) |
29 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β (mVarsβπ‘) = (mVarsβπ)) |
30 | | mclsval.v |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (mVarsβπ) |
31 | 29, 30 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π β (mVarsβπ‘) = π) |
32 | 14 | fveq1d 6841 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β ((mVHβπ‘)βπ₯) = (π»βπ₯)) |
33 | 32 | fveq2d 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π β (π β((mVHβπ‘)βπ₯)) = (π β(π»βπ₯))) |
34 | 31, 33 | fveq12d 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π β ((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) = (πβ(π β(π»βπ₯)))) |
35 | 14 | fveq1d 6841 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β ((mVHβπ‘)βπ¦) = (π»βπ¦)) |
36 | 35 | fveq2d 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π β (π β((mVHβπ‘)βπ¦)) = (π β(π»βπ¦))) |
37 | 31, 36 | fveq12d 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π β ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦))) = (πβ(π β(π»βπ¦)))) |
38 | 34, 37 | xpeq12d 5662 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = π β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) = ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦))))) |
39 | 38 | sseq1d 3973 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = π β ((((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) |
40 | 39 | imbi2d 340 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = π β ((π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π) β (π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π))) |
41 | 40 | 2albidv 1926 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β (βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π) β βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π))) |
42 | 28, 41 | anbi12d 631 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β (((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β ((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)))) |
43 | 42 | imbi1d 341 |
. . . . . . . . . . . . 13
β’ (π‘ = π β ((((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π) β (((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π))) |
44 | 25, 43 | raleqbidv 3317 |
. . . . . . . . . . . 12
β’ (π‘ = π β (βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π) β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π))) |
45 | 21, 44 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π‘ = π β ((β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)) β (β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))) |
46 | 45 | albidv 1923 |
. . . . . . . . . 10
β’ (π‘ = π β (βπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)) β βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))) |
47 | 46 | 2albidv 1926 |
. . . . . . . . 9
β’ (π‘ = π β (βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)) β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))) |
48 | 17, 47 | anbi12d 631 |
. . . . . . . 8
β’ (π‘ = π β (((β βͺ ran (mVHβπ‘)) β π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π))) β ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π))))) |
49 | 48 | abbidv 2806 |
. . . . . . 7
β’ (π‘ = π β {π β£ ((β βͺ ran (mVHβπ‘)) β π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))} = {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))}) |
50 | 49 | inteqd 4910 |
. . . . . 6
β’ (π‘ = π β β© {π β£ ((β βͺ ran (mVHβπ‘)) β π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))} = β© {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))}) |
51 | 7, 11, 50 | mpoeq123dv 7426 |
. . . . 5
β’ (π‘ = π β (π β π« (mDVβπ‘), β β π« (mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))}) = (π β π« π·, β β π« πΈ β¦ β© {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))})) |
52 | | df-mcls 33903 |
. . . . 5
β’ mCls =
(π‘ β V β¦ (π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))})) |
53 | 5 | fvexi 6853 |
. . . . . . 7
β’ π· β V |
54 | 53 | pwex 5333 |
. . . . . 6
β’ π«
π· β V |
55 | 9 | fvexi 6853 |
. . . . . . 7
β’ πΈ β V |
56 | 55 | pwex 5333 |
. . . . . 6
β’ π«
πΈ β V |
57 | 54, 56 | mpoex 8004 |
. . . . 5
β’ (π β π« π·, β β π« πΈ β¦ β© {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))}) β V |
58 | 51, 52, 57 | fvmpt 6945 |
. . . 4
β’ (π β V β
(mClsβπ) = (π β π« π·, β β π« πΈ β¦ β© {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))})) |
59 | 2, 3, 58 | 3syl 18 |
. . 3
β’ (π β (mClsβπ) = (π β π« π·, β β π« πΈ β¦ β© {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))})) |
60 | 1, 59 | eqtrid 2789 |
. 2
β’ (π β πΆ = (π β π« π·, β β π« πΈ β¦ β© {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))})) |
61 | | simprr 771 |
. . . . . . 7
β’ ((π β§ (π = πΎ β§ β = π΅)) β β = π΅) |
62 | 61 | uneq1d 4120 |
. . . . . 6
β’ ((π β§ (π = πΎ β§ β = π΅)) β (β βͺ ran π») = (π΅ βͺ ran π»)) |
63 | 62 | sseq1d 3973 |
. . . . 5
β’ ((π β§ (π = πΎ β§ β = π΅)) β ((β βͺ ran π») β π β (π΅ βͺ ran π») β π)) |
64 | | simprl 769 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π = πΎ β§ β = π΅)) β π = πΎ) |
65 | 64 | sseq2d 3974 |
. . . . . . . . . . . . 13
β’ ((π β§ (π = πΎ β§ β = π΅)) β (((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) |
66 | 65 | imbi2d 340 |
. . . . . . . . . . . 12
β’ ((π β§ (π = πΎ β§ β = π΅)) β ((π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π) β (π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ))) |
67 | 66 | 2albidv 1926 |
. . . . . . . . . . 11
β’ ((π β§ (π = πΎ β§ β = π΅)) β (βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π) β βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ))) |
68 | 67 | anbi2d 629 |
. . . . . . . . . 10
β’ ((π β§ (π = πΎ β§ β = π΅)) β (((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β ((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)))) |
69 | 68 | imbi1d 341 |
. . . . . . . . 9
β’ ((π β§ (π = πΎ β§ β = π΅)) β ((((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π) β (((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π))) |
70 | 69 | ralbidv 3172 |
. . . . . . . 8
β’ ((π β§ (π = πΎ β§ β = π΅)) β (βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π) β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π))) |
71 | 70 | imbi2d 340 |
. . . . . . 7
β’ ((π β§ (π = πΎ β§ β = π΅)) β ((β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)) β (β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))) |
72 | 71 | albidv 1923 |
. . . . . 6
β’ ((π β§ (π = πΎ β§ β = π΅)) β (βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)) β βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))) |
73 | 72 | 2albidv 1926 |
. . . . 5
β’ ((π β§ (π = πΎ β§ β = π΅)) β (βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)) β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))) |
74 | 63, 73 | anbi12d 631 |
. . . 4
β’ ((π β§ (π = πΎ β§ β = π΅)) β (((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π))) β ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π))))) |
75 | 74 | abbidv 2806 |
. . 3
β’ ((π β§ (π = πΎ β§ β = π΅)) β {π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))} = {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) |
76 | 75 | inteqd 4910 |
. 2
β’ ((π β§ (π = πΎ β§ β = π΅)) β β©
{π β£ ((β βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β π)) β (π βπ) β π)))} = β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) |
77 | | mclsval.2 |
. . 3
β’ (π β πΎ β π·) |
78 | 53 | elpw2 5300 |
. . 3
β’ (πΎ β π« π· β πΎ β π·) |
79 | 77, 78 | sylibr 233 |
. 2
β’ (π β πΎ β π« π·) |
80 | | mclsval.3 |
. . 3
β’ (π β π΅ β πΈ) |
81 | 55 | elpw2 5300 |
. . 3
β’ (π΅ β π« πΈ β π΅ β πΈ) |
82 | 80, 81 | sylibr 233 |
. 2
β’ (π β π΅ β π« πΈ) |
83 | 5, 9, 1, 2, 77, 80, 13, 19, 23, 30 | mclsssvlem 33968 |
. . 3
β’ (π β β© {π
β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ) |
84 | 55 | ssex 5276 |
. . 3
β’ (β© {π
β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ β β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β V) |
85 | 83, 84 | syl 17 |
. 2
β’ (π β β© {π
β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β V) |
86 | 60, 76, 79, 82, 85 | ovmpod 7501 |
1
β’ (π β (πΎπΆπ΅) = β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) |