Step | Hyp | Ref
| Expression |
1 | | n0i 4334 |
. . 3
β’ (π΄ β (πΎπΆπ΅) β Β¬ (πΎπΆπ΅) = β
) |
2 | | mclsval.c |
. . . . . 6
β’ πΆ = (mClsβπ) |
3 | | fvprc 6884 |
. . . . . 6
β’ (Β¬
π β V β
(mClsβπ) =
β
) |
4 | 2, 3 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β πΆ = β
) |
5 | 4 | oveqd 7426 |
. . . 4
β’ (Β¬
π β V β (πΎπΆπ΅) = (πΎβ
π΅)) |
6 | | 0ov 7446 |
. . . 4
β’ (πΎβ
π΅) = β
|
7 | 5, 6 | eqtrdi 2789 |
. . 3
β’ (Β¬
π β V β (πΎπΆπ΅) = β
) |
8 | 1, 7 | nsyl2 141 |
. 2
β’ (π΄ β (πΎπΆπ΅) β π β V) |
9 | | fveq2 6892 |
. . . . . . . . 9
β’ (π‘ = π β (mClsβπ‘) = (mClsβπ)) |
10 | 9, 2 | eqtr4di 2791 |
. . . . . . . 8
β’ (π‘ = π β (mClsβπ‘) = πΆ) |
11 | 10 | oveqd 7426 |
. . . . . . 7
β’ (π‘ = π β (πΎ(mClsβπ‘)π΅) = (πΎπΆπ΅)) |
12 | 11 | eleq2d 2820 |
. . . . . 6
β’ (π‘ = π β (π΄ β (πΎ(mClsβπ‘)π΅) β π΄ β (πΎπΆπ΅))) |
13 | | fvex 6905 |
. . . . . . . . 9
β’
(mDVβπ‘) β
V |
14 | 13 | elpw2 5346 |
. . . . . . . 8
β’ (πΎ β π«
(mDVβπ‘) β πΎ β (mDVβπ‘)) |
15 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π‘ = π β (mDVβπ‘) = (mDVβπ)) |
16 | | mclsval.d |
. . . . . . . . . 10
β’ π· = (mDVβπ) |
17 | 15, 16 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π‘ = π β (mDVβπ‘) = π·) |
18 | 17 | sseq2d 4015 |
. . . . . . . 8
β’ (π‘ = π β (πΎ β (mDVβπ‘) β πΎ β π·)) |
19 | 14, 18 | bitrid 283 |
. . . . . . 7
β’ (π‘ = π β (πΎ β π« (mDVβπ‘) β πΎ β π·)) |
20 | | fvex 6905 |
. . . . . . . . 9
β’
(mExβπ‘) β
V |
21 | 20 | elpw2 5346 |
. . . . . . . 8
β’ (π΅ β π«
(mExβπ‘) β π΅ β (mExβπ‘)) |
22 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π‘ = π β (mExβπ‘) = (mExβπ)) |
23 | | mclsval.e |
. . . . . . . . . 10
β’ πΈ = (mExβπ) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π‘ = π β (mExβπ‘) = πΈ) |
25 | 24 | sseq2d 4015 |
. . . . . . . 8
β’ (π‘ = π β (π΅ β (mExβπ‘) β π΅ β πΈ)) |
26 | 21, 25 | bitrid 283 |
. . . . . . 7
β’ (π‘ = π β (π΅ β π« (mExβπ‘) β π΅ β πΈ)) |
27 | 19, 26 | anbi12d 632 |
. . . . . 6
β’ (π‘ = π β ((πΎ β π« (mDVβπ‘) β§ π΅ β π« (mExβπ‘)) β (πΎ β π· β§ π΅ β πΈ))) |
28 | 12, 27 | imbi12d 345 |
. . . . 5
β’ (π‘ = π β ((π΄ β (πΎ(mClsβπ‘)π΅) β (πΎ β π« (mDVβπ‘) β§ π΅ β π« (mExβπ‘))) β (π΄ β (πΎπΆπ΅) β (πΎ β π· β§ π΅ β πΈ)))) |
29 | | vex 3479 |
. . . . . . 7
β’ π‘ β V |
30 | 13 | pwex 5379 |
. . . . . . . 8
β’ π«
(mDVβπ‘) β
V |
31 | 20 | pwex 5379 |
. . . . . . . 8
β’ π«
(mExβπ‘) β
V |
32 | 30, 31 | mpoex 8066 |
. . . . . . 7
β’ (π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))}) β V |
33 | | df-mcls 34488 |
. . . . . . . 8
β’ mCls =
(π‘ β V β¦ (π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))})) |
34 | 33 | fvmpt2 7010 |
. . . . . . 7
β’ ((π‘ β V β§ (π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))}) β V) β (mClsβπ‘) = (π β π« (mDVβπ‘), β β π« (mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))})) |
35 | 29, 32, 34 | mp2an 691 |
. . . . . 6
β’
(mClsβπ‘) =
(π β π«
(mDVβπ‘), β β π«
(mExβπ‘) β¦ β© {π
β£ ((β βͺ ran
(mVHβπ‘)) β
π β§ βπβπβπ(β¨π, π, πβ© β (mAxβπ‘) β βπ β ran (mSubstβπ‘)(((π β (π βͺ ran (mVHβπ‘))) β π β§ βπ₯βπ¦(π₯ππ¦ β (((mVarsβπ‘)β(π β((mVHβπ‘)βπ₯))) Γ ((mVarsβπ‘)β(π β((mVHβπ‘)βπ¦)))) β π)) β (π βπ) β π)))}) |
36 | 35 | elmpocl 7648 |
. . . . 5
β’ (π΄ β (πΎ(mClsβπ‘)π΅) β (πΎ β π« (mDVβπ‘) β§ π΅ β π« (mExβπ‘))) |
37 | 28, 36 | vtoclg 3557 |
. . . 4
β’ (π β V β (π΄ β (πΎπΆπ΅) β (πΎ β π· β§ π΅ β πΈ))) |
38 | 8, 37 | mpcom 38 |
. . 3
β’ (π΄ β (πΎπΆπ΅) β (πΎ β π· β§ π΅ β πΈ)) |
39 | 38 | simpld 496 |
. 2
β’ (π΄ β (πΎπΆπ΅) β πΎ β π·) |
40 | 38 | simprd 497 |
. 2
β’ (π΄ β (πΎπΆπ΅) β π΅ β πΈ) |
41 | 8, 39, 40 | 3jca 1129 |
1
β’ (π΄ β (πΎπΆπ΅) β (π β V β§ πΎ β π· β§ π΅ β πΈ)) |