Step | Hyp | Ref
| Expression |
1 | | mclsval.3 |
. . . 4
β’ (π β π΅ β πΈ) |
2 | | mclsval.1 |
. . . . . 6
β’ (π β π β mFS) |
3 | | eqid 2733 |
. . . . . . 7
β’
(mVRβπ) =
(mVRβπ) |
4 | | mclsval.e |
. . . . . . 7
β’ πΈ = (mExβπ) |
5 | | mclsval.h |
. . . . . . 7
β’ π» = (mVHβπ) |
6 | 3, 4, 5 | mvhf 34216 |
. . . . . 6
β’ (π β mFS β π»:(mVRβπ)βΆπΈ) |
7 | 2, 6 | syl 17 |
. . . . 5
β’ (π β π»:(mVRβπ)βΆπΈ) |
8 | 7 | frnd 6680 |
. . . 4
β’ (π β ran π» β πΈ) |
9 | 1, 8 | unssd 4150 |
. . 3
β’ (π β (π΅ βͺ ran π») β πΈ) |
10 | | mclsval.s |
. . . . . . . . . 10
β’ π = (mSubstβπ) |
11 | 10, 4 | msubf 34190 |
. . . . . . . . 9
β’ (π β ran π β π :πΈβΆπΈ) |
12 | | mclsval.a |
. . . . . . . . . . . . . 14
β’ π΄ = (mAxβπ) |
13 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(mStatβπ) =
(mStatβπ) |
14 | 12, 13 | maxsta 34212 |
. . . . . . . . . . . . 13
β’ (π β mFS β π΄ β (mStatβπ)) |
15 | 2, 14 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π΄ β (mStatβπ)) |
16 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(mPreStβπ) =
(mPreStβπ) |
17 | 16, 13 | mstapst 34205 |
. . . . . . . . . . . 12
β’
(mStatβπ)
β (mPreStβπ) |
18 | 15, 17 | sstrdi 3960 |
. . . . . . . . . . 11
β’ (π β π΄ β (mPreStβπ)) |
19 | 18 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ β¨π, π, πβ© β π΄) β β¨π, π, πβ© β (mPreStβπ)) |
20 | | mclsval.d |
. . . . . . . . . . . 12
β’ π· = (mDVβπ) |
21 | 20, 4, 16 | elmpst 34194 |
. . . . . . . . . . 11
β’
(β¨π, π, πβ© β (mPreStβπ) β ((π β π· β§ β‘π = π) β§ (π β πΈ β§ π β Fin) β§ π β πΈ)) |
22 | 21 | simp3bi 1148 |
. . . . . . . . . 10
β’
(β¨π, π, πβ© β (mPreStβπ) β π β πΈ) |
23 | 19, 22 | syl 17 |
. . . . . . . . 9
β’ ((π β§ β¨π, π, πβ© β π΄) β π β πΈ) |
24 | | ffvelcdm 7036 |
. . . . . . . . 9
β’ ((π :πΈβΆπΈ β§ π β πΈ) β (π βπ) β πΈ) |
25 | 11, 23, 24 | syl2anr 598 |
. . . . . . . 8
β’ (((π β§ β¨π, π, πβ© β π΄) β§ π β ran π) β (π βπ) β πΈ) |
26 | 25 | a1d 25 |
. . . . . . 7
β’ (((π β§ β¨π, π, πβ© β π΄) β§ π β ran π) β (((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)) |
27 | 26 | ralrimiva 3140 |
. . . . . 6
β’ ((π β§ β¨π, π, πβ© β π΄) β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)) |
28 | 27 | ex 414 |
. . . . 5
β’ (π β (β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
29 | 28 | alrimiv 1931 |
. . . 4
β’ (π β βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
30 | 29 | alrimivv 1932 |
. . 3
β’ (π β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
31 | 4 | fvexi 6860 |
. . . 4
β’ πΈ β V |
32 | | sseq2 3974 |
. . . . 5
β’ (π = πΈ β ((π΅ βͺ ran π») β π β (π΅ βͺ ran π») β πΈ)) |
33 | | sseq2 3974 |
. . . . . . . . . . 11
β’ (π = πΈ β ((π β (π βͺ ran π»)) β π β (π β (π βͺ ran π»)) β πΈ)) |
34 | 33 | anbi1d 631 |
. . . . . . . . . 10
β’ (π = πΈ β (((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β ((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)))) |
35 | | eleq2 2823 |
. . . . . . . . . 10
β’ (π = πΈ β ((π βπ) β π β (π βπ) β πΈ)) |
36 | 34, 35 | imbi12d 345 |
. . . . . . . . 9
β’ (π = πΈ β ((((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β (((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
37 | 36 | ralbidv 3171 |
. . . . . . . 8
β’ (π = πΈ β (βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π) β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))) |
38 | 37 | imbi2d 341 |
. . . . . . 7
β’ (π = πΈ β ((β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β (β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
39 | 38 | albidv 1924 |
. . . . . 6
β’ (π = πΈ β (βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β βπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
40 | 39 | 2albidv 1927 |
. . . . 5
β’ (π = πΈ β (βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)) β βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
41 | 32, 40 | anbi12d 632 |
. . . 4
β’ (π = πΈ β (((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π))) β ((π΅ βͺ ran π») β πΈ β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ))))) |
42 | 31, 41 | elab 3634 |
. . 3
β’ (πΈ β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β ((π΅ βͺ ran π») β πΈ β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β πΈ β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β πΈ)))) |
43 | 9, 30, 42 | sylanbrc 584 |
. 2
β’ (π β πΈ β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))}) |
44 | | intss1 4928 |
. 2
β’ (πΈ β {π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β β©
{π β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ) |
45 | 43, 44 | syl 17 |
1
β’ (π β β© {π
β£ ((π΅ βͺ ran π») β π β§ βπβπβπ(β¨π, π, πβ© β π΄ β βπ β ran π(((π β (π βͺ ran π»)) β π β§ βπ₯βπ¦(π₯ππ¦ β ((πβ(π β(π»βπ₯))) Γ (πβ(π β(π»βπ¦)))) β πΎ)) β (π βπ) β π)))} β πΈ) |