Step | Hyp | Ref
| Expression |
1 | | mclspps.5 |
. . . 4
β’ (π β π β ran πΏ) |
2 | | mclspps.l |
. . . . 5
β’ πΏ = (mSubstβπ) |
3 | | mclspps.e |
. . . . 5
β’ πΈ = (mExβπ) |
4 | 2, 3 | msubf 34523 |
. . . 4
β’ (π β ran πΏ β π:πΈβΆπΈ) |
5 | 1, 4 | syl 17 |
. . 3
β’ (π β π:πΈβΆπΈ) |
6 | 5 | ffnd 6719 |
. 2
β’ (π β π Fn πΈ) |
7 | | mclspps.d |
. . . 4
β’ π· = (mDVβπ) |
8 | | mclspps.c |
. . . 4
β’ πΆ = (mClsβπ) |
9 | | mclspps.1 |
. . . 4
β’ (π β π β mFS) |
10 | | eqid 2733 |
. . . . . . . . 9
β’
(mPreStβπ) =
(mPreStβπ) |
11 | | mclspps.j |
. . . . . . . . 9
β’ π½ = (mPPStβπ) |
12 | 10, 11 | mppspst 34565 |
. . . . . . . 8
β’ π½ β (mPreStβπ) |
13 | | mclspps.4 |
. . . . . . . 8
β’ (π β β¨π, π, πβ© β π½) |
14 | 12, 13 | sselid 3981 |
. . . . . . 7
β’ (π β β¨π, π, πβ© β (mPreStβπ)) |
15 | 7, 3, 10 | elmpst 34527 |
. . . . . . 7
β’
(β¨π, π, πβ© β (mPreStβπ) β ((π β π· β§ β‘π = π) β§ (π β πΈ β§ π β Fin) β§ π β πΈ)) |
16 | 14, 15 | sylib 217 |
. . . . . 6
β’ (π β ((π β π· β§ β‘π = π) β§ (π β πΈ β§ π β Fin) β§ π β πΈ)) |
17 | 16 | simp1d 1143 |
. . . . 5
β’ (π β (π β π· β§ β‘π = π)) |
18 | 17 | simpld 496 |
. . . 4
β’ (π β π β π·) |
19 | 16 | simp2d 1144 |
. . . . 5
β’ (π β (π β πΈ β§ π β Fin)) |
20 | 19 | simpld 496 |
. . . 4
β’ (π β π β πΈ) |
21 | | eqid 2733 |
. . . 4
β’
(mAxβπ) =
(mAxβπ) |
22 | | mclspps.v |
. . . 4
β’ π = (mVRβπ) |
23 | | mclspps.h |
. . . 4
β’ π» = (mVHβπ) |
24 | | mclspps.w |
. . . 4
β’ π = (mVarsβπ) |
25 | | mclspps.6 |
. . . . . 6
β’ ((π β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) |
26 | 25 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ₯ β π (πβπ₯) β (πΎπΆπ΅)) |
27 | 5 | ffund 6722 |
. . . . . 6
β’ (π β Fun π) |
28 | 5 | fdmd 6729 |
. . . . . . 7
β’ (π β dom π = πΈ) |
29 | 20, 28 | sseqtrrd 4024 |
. . . . . 6
β’ (π β π β dom π) |
30 | | funimass5 7057 |
. . . . . 6
β’ ((Fun
π β§ π β dom π) β (π β (β‘π β (πΎπΆπ΅)) β βπ₯ β π (πβπ₯) β (πΎπΆπ΅))) |
31 | 27, 29, 30 | syl2anc 585 |
. . . . 5
β’ (π β (π β (β‘π β (πΎπΆπ΅)) β βπ₯ β π (πβπ₯) β (πΎπΆπ΅))) |
32 | 26, 31 | mpbird 257 |
. . . 4
β’ (π β π β (β‘π β (πΎπΆπ΅))) |
33 | 22, 3, 23 | mvhf 34549 |
. . . . . . 7
β’ (π β mFS β π»:πβΆπΈ) |
34 | 9, 33 | syl 17 |
. . . . . 6
β’ (π β π»:πβΆπΈ) |
35 | 34 | ffvelcdmda 7087 |
. . . . 5
β’ ((π β§ π£ β π) β (π»βπ£) β πΈ) |
36 | | mclspps.7 |
. . . . 5
β’ ((π β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) |
37 | | elpreima 7060 |
. . . . . . 7
β’ (π Fn πΈ β ((π»βπ£) β (β‘π β (πΎπΆπ΅)) β ((π»βπ£) β πΈ β§ (πβ(π»βπ£)) β (πΎπΆπ΅)))) |
38 | 6, 37 | syl 17 |
. . . . . 6
β’ (π β ((π»βπ£) β (β‘π β (πΎπΆπ΅)) β ((π»βπ£) β πΈ β§ (πβ(π»βπ£)) β (πΎπΆπ΅)))) |
39 | 38 | adantr 482 |
. . . . 5
β’ ((π β§ π£ β π) β ((π»βπ£) β (β‘π β (πΎπΆπ΅)) β ((π»βπ£) β πΈ β§ (πβ(π»βπ£)) β (πΎπΆπ΅)))) |
40 | 35, 36, 39 | mpbir2and 712 |
. . . 4
β’ ((π β§ π£ β π) β (π»βπ£) β (β‘π β (πΎπΆπ΅))) |
41 | 9 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β π β mFS) |
42 | | mclspps.2 |
. . . . . 6
β’ (π β πΎ β π·) |
43 | 42 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β πΎ β π·) |
44 | | mclspps.3 |
. . . . . 6
β’ (π β π΅ β πΈ) |
45 | 44 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β π΅ β πΈ) |
46 | 13 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β β¨π, π, πβ© β π½) |
47 | 1 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β π β ran πΏ) |
48 | 25 | 3ad2antl1 1186 |
. . . . 5
β’ (((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β§ π₯ β π) β (πβπ₯) β (πΎπΆπ΅)) |
49 | 36 | 3ad2antl1 1186 |
. . . . 5
β’ (((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β§ π£ β π) β (πβ(π»βπ£)) β (πΎπΆπ΅)) |
50 | | mclspps.8 |
. . . . . 6
β’ ((π β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) |
51 | 50 | 3ad2antl1 1186 |
. . . . 5
β’ (((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β§ (π₯ππ¦ β§ π β (πβ(πβ(π»βπ₯))) β§ π β (πβ(πβ(π»βπ¦))))) β ππΎπ) |
52 | | simp21 1207 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β β¨π, π, πβ© β (mAxβπ)) |
53 | | simp22 1208 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β π β ran πΏ) |
54 | | simp23 1209 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) |
55 | | simp3 1139 |
. . . . 5
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) |
56 | 7, 3, 8, 41, 43, 45, 11, 2, 22, 23, 24, 46, 47, 48, 49, 51, 52, 53, 54, 55 | mclsppslem 34574 |
. . . 4
β’ ((π β§ (β¨π, π, πβ© β (mAxβπ) β§ π β ran πΏ β§ (π β (π βͺ ran π»)) β (β‘π β (πΎπΆπ΅))) β§ βπ§βπ€(π§ππ€ β ((πβ(π β(π»βπ§))) Γ (πβ(π β(π»βπ€)))) β π)) β (π βπ) β (β‘π β (πΎπΆπ΅))) |
57 | 7, 3, 8, 9, 18, 20, 21, 2, 22, 23, 24, 32, 40, 56 | mclsind 34561 |
. . 3
β’ (π β (ππΆπ) β (β‘π β (πΎπΆπ΅))) |
58 | 10, 11, 8 | elmpps 34564 |
. . . . 5
β’
(β¨π, π, πβ© β π½ β (β¨π, π, πβ© β (mPreStβπ) β§ π β (ππΆπ))) |
59 | 58 | simprbi 498 |
. . . 4
β’
(β¨π, π, πβ© β π½ β π β (ππΆπ)) |
60 | 13, 59 | syl 17 |
. . 3
β’ (π β π β (ππΆπ)) |
61 | 57, 60 | sseldd 3984 |
. 2
β’ (π β π β (β‘π β (πΎπΆπ΅))) |
62 | | elpreima 7060 |
. . 3
β’ (π Fn πΈ β (π β (β‘π β (πΎπΆπ΅)) β (π β πΈ β§ (πβπ) β (πΎπΆπ΅)))) |
63 | 62 | simplbda 501 |
. 2
β’ ((π Fn πΈ β§ π β (β‘π β (πΎπΆπ΅))) β (πβπ) β (πΎπΆπ΅)) |
64 | 6, 61, 63 | syl2anc 585 |
1
β’ (π β (πβπ) β (πΎπΆπ΅)) |