Step | Hyp | Ref
| Expression |
1 | | mclsval.3 |
. . . 4
β’ (π β π΅ β πΈ) |
2 | | mclsval.1 |
. . . . . 6
β’ (π β π β mFS) |
3 | | eqid 2732 |
. . . . . . 7
β’
(mVRβπ) =
(mVRβπ) |
4 | | mclsval.e |
. . . . . . 7
β’ πΈ = (mExβπ) |
5 | | mclsval.h |
. . . . . . 7
β’ π» = (mVHβπ) |
6 | 3, 4, 5 | mvhf 34544 |
. . . . . 6
β’ (π β mFS β π»:(mVRβπ)βΆπΈ) |
7 | 2, 6 | syl 17 |
. . . . 5
β’ (π β π»:(mVRβπ)βΆπΈ) |
8 | 7 | frnd 6725 |
. . . 4
β’ (π β ran π» β πΈ) |
9 | 1, 8 | unssd 4186 |
. . 3
β’ (π β (π΅ βͺ ran π») β πΈ) |
10 | | mclsval.s |
. . . . . . . . . 10
β’ π = (mSubstβπ) |
11 | 10, 4 | msubf 34518 |
. . . . . . . . 9
β’ (π β ran π β π :πΈβΆπΈ) |
12 | | mclsval.a |
. . . . . . . . . . . . . 14
β’ π΄ = (mAxβπ) |
13 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(mStatβπ) =
(mStatβπ) |
14 | 12, 13 | maxsta 34540 |
. . . . . . . . . . . . 13
β’ (π β mFS β π΄ β (mStatβπ)) |
15 | 2, 14 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π΄ β (mStatβπ)) |
16 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(mPreStβπ) =
(mPreStβπ) |
17 | 16, 13 | mstapst 34533 |
. . . . . . . . . . . 12
β’
(mStatβπ)
β (mPreStβπ) |
18 | 15, 17 | sstrdi 3994 |
. . . . . . . . . . 11
β’ (π β π΄ β (mPreStβπ)) |
19 | 18 | sselda 3982 |
. . . . . . . . . 10
β’ ((π β§ β¨π, π, πβ© β π΄) β β¨π, π, πβ© β (mPreStβπ)) |
20 | | mclsval.d |
. . . . . . . . . . . 12
β’ π· = (mDVβπ) |
21 | 20, 4, 16 | elmpst 34522 |
. . . . . . . . . . 11
β’
(β¨π, π, πβ© β (mPreStβπ) β ((π β π· β§ β‘π = π) β§ (π β πΈ β§ π β Fin) β§ π β πΈ)) |
22 | 21 | simp3bi 1147 |
. . . . . . . . . 10
β’
(β¨π, π, πβ© β (mPreStβπ) β π β πΈ) |
23 | 19, 22 | syl 17 |
. . . . . . . . 9
β’ ((π β§ β¨π, π, πβ© β π΄) β π β πΈ) |
24 | | ffvelcdm 7083 |
. . . . . . . . 9
β’ ((π :πΈβΆπΈ β§ π β πΈ) β (π βπ) β πΈ) |
25 | 11, 23, 24 | syl2anr 597 |
. . . . . . . 8
β’ (((π β§ β¨π, π, πβ© β π΄) β§ π β ran π) β (π βπ) β πΈ) |
26 | 25 | a1d 25 |
. . . . . . 7
β’ (((π β§ β¨π, π, πβ© β π΄) β§ π β ran π) β (((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)) |
27 | 26 | ralrimiva 3146 |
. . . . . 6
β’ ((π β§ β¨π, π, πβ© β π΄) β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)) |
28 | 27 | ex 413 |
. . . . 5
β’ (π β (β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
29 | 28 | alrimiv 1930 |
. . . 4
β’ (π β βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
30 | 29 | alrimivv 1931 |
. . 3
β’ (π β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
31 | 4 | fvexi 6905 |
. . . 4
β’ πΈ β V |
32 | | sseq2 4008 |
. . . . 5
β’ (π = πΈ β ((π΅ βͺ ran π») β π β (π΅ βͺ ran π») β πΈ)) |
33 | | sseq2 4008 |
. . . . . . . . . . 11
β’ (π = πΈ β ((π β (π βͺ ran π»)) β π β (π β (π βͺ ran π»)) β πΈ)) |
34 | 33 | anbi1d 630 |
. . . . . . . . . 10
β’ (π = πΈ β (((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β ((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)))) |
35 | | eleq2 2822 |
. . . . . . . . . 10
β’ (π = πΈ β ((π βπ) β π β (π βπ) β πΈ)) |
36 | 34, 35 | imbi12d 344 |
. . . . . . . . 9
β’ (π = πΈ β ((((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β (((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
37 | 36 | ralbidv 3177 |
. . . . . . . 8
β’ (π = πΈ β (βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
38 | 37 | imbi2d 340 |
. . . . . . 7
β’ (π = πΈ β ((β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β (β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
39 | 38 | albidv 1923 |
. . . . . 6
β’ (π = πΈ β (βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
40 | 39 | 2albidv 1926 |
. . . . 5
β’ (π = πΈ β (βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
41 | 32, 40 | anbi12d 631 |
. . . 4
β’ (π = πΈ β (((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π))) β ((π΅ βͺ ran π») β πΈ β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))))) |
42 | 31, 41 | elab 3668 |
. . 3
β’ (πΈ β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β ((π΅ βͺ ran π») β πΈ β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
43 | 9, 30, 42 | sylanbrc 583 |
. 2
β’ (π β πΈ β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) |
44 | | intss1 4967 |
. 2
β’ (πΈ β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β β©
{π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ) |
45 | 43, 44 | syl 17 |
1
β’ (π β β© {π
β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ) |