Step | Hyp | Ref
| Expression |
1 | | mclsval.d |
. . 3
β’ π· = (mDVβπ) |
2 | | mclsval.e |
. . 3
β’ πΈ = (mExβπ) |
3 | | mclsval.c |
. . 3
β’ πΆ = (mClsβπ) |
4 | | mclsval.1 |
. . 3
β’ (π β π β mFS) |
5 | | mclsval.2 |
. . 3
β’ (π β πΎ β π·) |
6 | | mclsval.3 |
. . 3
β’ (π β π΅ β πΈ) |
7 | | mclsax.h |
. . 3
β’ π» = (mVHβπ) |
8 | | mclsax.a |
. . 3
β’ π΄ = (mAxβπ) |
9 | | mclsax.l |
. . 3
β’ πΏ = (mSubstβπ) |
10 | | mclsax.w |
. . 3
β’ π = (mVarsβπ) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | mclsval 34221 |
. 2
β’ (π β (πΎπΆπ΅) = β© {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) |
12 | | mclsind.4 |
. . . . . . 7
β’ (π β π΅ β π) |
13 | 6, 12 | ssind 4196 |
. . . . . 6
β’ (π β π΅ β (πΈ β© π)) |
14 | | mclsax.v |
. . . . . . . . . . 11
β’ π = (mVRβπ) |
15 | 14, 2, 7 | mvhf 34216 |
. . . . . . . . . 10
β’ (π β mFS β π»:πβΆπΈ) |
16 | 4, 15 | syl 17 |
. . . . . . . . 9
β’ (π β π»:πβΆπΈ) |
17 | 16 | ffnd 6673 |
. . . . . . . 8
β’ (π β π» Fn π) |
18 | 16 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π£ β π) β (π»βπ£) β πΈ) |
19 | | mclsind.5 |
. . . . . . . . . 10
β’ ((π β§ π£ β π) β (π»βπ£) β π) |
20 | 18, 19 | elind 4158 |
. . . . . . . . 9
β’ ((π β§ π£ β π) β (π»βπ£) β (πΈ β© π)) |
21 | 20 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ£ β π (π»βπ£) β (πΈ β© π)) |
22 | | ffnfv 7070 |
. . . . . . . 8
β’ (π»:πβΆ(πΈ β© π) β (π» Fn π β§ βπ£ β π (π»βπ£) β (πΈ β© π))) |
23 | 17, 21, 22 | sylanbrc 584 |
. . . . . . 7
β’ (π β π»:πβΆ(πΈ β© π)) |
24 | 23 | frnd 6680 |
. . . . . 6
β’ (π β ran π» β (πΈ β© π)) |
25 | 13, 24 | unssd 4150 |
. . . . 5
β’ (π β (π΅ βͺ ran π») β (πΈ β© π)) |
26 | | id 22 |
. . . . . . . . . . . 12
β’ ((π β (π βͺ ran π»)) β (πΈ β© π) β (π β (π βͺ ran π»)) β (πΈ β© π)) |
27 | | inss2 4193 |
. . . . . . . . . . . 12
β’ (πΈ β© π) β π |
28 | 26, 27 | sstrdi 3960 |
. . . . . . . . . . 11
β’ ((π β (π βͺ ran π»)) β (πΈ β© π) β (π β (π βͺ ran π»)) β π) |
29 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β π β mFS) |
30 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(mRExβπ) =
(mRExβπ) |
31 | 14, 30, 9, 2 | msubff 34188 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β mFS β πΏ:((mRExβπ) βpm π)βΆ(πΈ βm πΈ)) |
32 | | frn 6679 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΏ:((mRExβπ) βpm π)βΆ(πΈ βm πΈ) β ran πΏ β (πΈ βm πΈ)) |
33 | 29, 31, 32 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β ran πΏ β (πΈ βm πΈ)) |
34 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β π β ran πΏ) |
35 | 33, 34 | sseldd 3949 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β π β (πΈ βm πΈ)) |
36 | | elmapi 8793 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΈ βm πΈ) β π :πΈβΆπΈ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β π :πΈβΆπΈ) |
38 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(mStatβπ) =
(mStatβπ) |
39 | 8, 38 | maxsta 34212 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β mFS β π΄ β (mStatβπ)) |
40 | 29, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β π΄ β (mStatβπ)) |
41 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(mPreStβπ) =
(mPreStβπ) |
42 | 41, 38 | mstapst 34205 |
. . . . . . . . . . . . . . . . . . . 20
β’
(mStatβπ)
β (mPreStβπ) |
43 | 40, 42 | sstrdi 3960 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β π΄ β (mPreStβπ)) |
44 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β β¨π, π, πβ© β π΄) |
45 | 43, 44 | sseldd 3949 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β β¨π, π, πβ© β (mPreStβπ)) |
46 | 1, 2, 41 | elmpst 34194 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨π, π, πβ© β (mPreStβπ) β ((π β π· β§ β‘π = π) β§ (π β πΈ β§ π β Fin) β§ π β πΈ)) |
47 | 46 | simp3bi 1148 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π, π, πβ© β (mPreStβπ) β π β πΈ) |
48 | 45, 47 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β π β πΈ) |
49 | 37, 48 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π)) β (π βπ) β πΈ) |
50 | 49 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ) |
51 | | mclsind.6 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) |
52 | 50, 51 | elind 4158 |
. . . . . . . . . . . . . 14
β’ ((π β§ (β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π)) |
53 | 52 | 3exp 1120 |
. . . . . . . . . . . . 13
β’ (π β ((β¨π, π, πβ© β π΄ β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β π) β (βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ) β (π βπ) β (πΈ β© π)))) |
54 | 53 | 3expd 1354 |
. . . . . . . . . . . 12
β’ (π β (β¨π, π, πβ© β π΄ β (π β ran πΏ β ((π β (π βͺ ran π»)) β π β (βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ) β (π βπ) β (πΈ β© π)))))) |
55 | 54 | imp31 419 |
. . . . . . . . . . 11
β’ (((π β§ β¨π, π, πβ© β π΄) β§ π β ran πΏ) β ((π β (π βͺ ran π»)) β π β (βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ) β (π βπ) β (πΈ β© π)))) |
56 | 28, 55 | syl5 34 |
. . . . . . . . . 10
β’ (((π β§ β¨π, π, πβ© β π΄) β§ π β ran πΏ) β ((π β (π βͺ ran π»)) β (πΈ β© π) β (βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ) β (π βπ) β (πΈ β© π)))) |
57 | 56 | impd 412 |
. . . . . . . . 9
β’ (((π β§ β¨π, π, πβ© β π΄) β§ π β ran πΏ) β (((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π))) |
58 | 57 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ β¨π, π, πβ© β π΄) β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π))) |
59 | 58 | ex 414 |
. . . . . . 7
β’ (π β (β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π)))) |
60 | 59 | alrimiv 1931 |
. . . . . 6
β’ (π β βπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π)))) |
61 | 60 | alrimivv 1932 |
. . . . 5
β’ (π β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π)))) |
62 | 2 | fvexi 6860 |
. . . . . . 7
β’ πΈ β V |
63 | 62 | inex1 5278 |
. . . . . 6
β’ (πΈ β© π) β V |
64 | | sseq2 3974 |
. . . . . . 7
β’ (π = (πΈ β© π) β ((π΅ βͺ ran π») β π β (π΅ βͺ ran π») β (πΈ β© π))) |
65 | | sseq2 3974 |
. . . . . . . . . . . . 13
β’ (π = (πΈ β© π) β ((π β (π βͺ ran π»)) β π β (π β (π βͺ ran π»)) β (πΈ β© π))) |
66 | 65 | anbi1d 631 |
. . . . . . . . . . . 12
β’ (π = (πΈ β© π) β (((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β ((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)))) |
67 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π = (πΈ β© π) β ((π βπ) β π β (π βπ) β (πΈ β© π))) |
68 | 66, 67 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = (πΈ β© π) β ((((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β (((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π)))) |
69 | 68 | ralbidv 3171 |
. . . . . . . . . 10
β’ (π = (πΈ β© π) β (βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π)))) |
70 | 69 | imbi2d 341 |
. . . . . . . . 9
β’ (π = (πΈ β© π) β ((β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β (β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π))))) |
71 | 70 | albidv 1924 |
. . . . . . . 8
β’ (π = (πΈ β© π) β (βπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β βπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π))))) |
72 | 71 | 2albidv 1927 |
. . . . . . 7
β’ (π = (πΈ β© π) β (βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π))))) |
73 | 64, 72 | anbi12d 632 |
. . . . . 6
β’ (π = (πΈ β© π) β (((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π))) β ((π΅ βͺ ran π») β (πΈ β© π) β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π)))))) |
74 | 63, 73 | elab 3634 |
. . . . 5
β’ ((πΈ β© π) β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β ((π΅ βͺ ran π») β (πΈ β© π) β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β (πΈ β© π) β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β (πΈ β© π))))) |
75 | 25, 61, 74 | sylanbrc 584 |
. . . 4
β’ (π β (πΈ β© π) β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) |
76 | | intss1 4928 |
. . . 4
β’ ((πΈ β© π) β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β β©
{π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β (πΈ β© π)) |
77 | 75, 76 | syl 17 |
. . 3
β’ (π β β© {π
β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β (πΈ β© π)) |
78 | 77, 27 | sstrdi 3960 |
. 2
β’ (π β β© {π
β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran πΏ(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β π) |
79 | 11, 78 | eqsstrd 3986 |
1
β’ (π β (πΎπΆπ΅) β π) |