Step | Hyp | Ref
| Expression |
1 | | msubvrs.e |
. . . . . 6
β’ πΈ = (mExβπ) |
2 | | eqid 2733 |
. . . . . 6
β’
(mRSubstβπ) =
(mRSubstβπ) |
3 | | msubvrs.s |
. . . . . 6
β’ π = (mSubstβπ) |
4 | 1, 2, 3 | elmsubrn 34550 |
. . . . 5
β’ ran π = ran (π β ran (mRSubstβπ) β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
5 | 4 | eleq2i 2826 |
. . . 4
β’ (πΉ β ran π β πΉ β ran (π β ran (mRSubstβπ) β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©))) |
6 | | eqid 2733 |
. . . . 5
β’ (π β ran (mRSubstβπ) β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) = (π β ran (mRSubstβπ) β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
7 | 1 | fvexi 6906 |
. . . . . 6
β’ πΈ β V |
8 | 7 | mptex 7225 |
. . . . 5
β’ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β
V |
9 | 6, 8 | elrnmpti 5960 |
. . . 4
β’ (πΉ β ran (π β ran (mRSubstβπ) β¦ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) β βπ β ran (mRSubstβπ)πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
10 | 5, 9 | bitri 275 |
. . 3
β’ (πΉ β ran π β βπ β ran (mRSubstβπ)πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)) |
11 | | simp2 1138 |
. . . . . . . . 9
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β π β ran (mRSubstβπ)) |
12 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β π β πΈ) |
13 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(mTCβπ) =
(mTCβπ) |
14 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(mRExβπ) =
(mRExβπ) |
15 | 13, 1, 14 | mexval 34524 |
. . . . . . . . . . 11
β’ πΈ = ((mTCβπ) Γ (mRExβπ)) |
16 | 12, 15 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β π β ((mTCβπ) Γ (mRExβπ))) |
17 | | xp2nd 8008 |
. . . . . . . . . 10
β’ (π β ((mTCβπ) Γ (mRExβπ)) β (2nd
βπ) β
(mRExβπ)) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (2nd βπ) β (mRExβπ)) |
19 | | eqid 2733 |
. . . . . . . . . 10
β’
(mVRβπ) =
(mVRβπ) |
20 | 2, 19, 14 | mrsubvrs 34544 |
. . . . . . . . 9
β’ ((π β ran (mRSubstβπ) β§ (2nd
βπ) β
(mRExβπ)) β (ran
(πβ(2nd
βπ)) β©
(mVRβπ)) = βͺ π₯ β (ran (2nd βπ) β© (mVRβπ))(ran (πββ¨βπ₯ββ©) β© (mVRβπ))) |
21 | 11, 18, 20 | syl2anc 585 |
. . . . . . . 8
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (ran (πβ(2nd βπ)) β© (mVRβπ)) = βͺ π₯ β (ran (2nd βπ) β© (mVRβπ))(ran (πββ¨βπ₯ββ©) β© (mVRβπ))) |
22 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π β (1st βπ) = (1st βπ)) |
23 | | 2fveq3 6897 |
. . . . . . . . . . . . 13
β’ (π = π β (πβ(2nd βπ)) = (πβ(2nd βπ))) |
24 | 22, 23 | opeq12d 4882 |
. . . . . . . . . . . 12
β’ (π = π β β¨(1st βπ), (πβ(2nd βπ))β© = β¨(1st
βπ), (πβ(2nd
βπ))β©) |
25 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) |
26 | | opex 5465 |
. . . . . . . . . . . 12
β’
β¨(1st βπ), (πβ(2nd βπ))β© β
V |
27 | 24, 25, 26 | fvmpt3i 7004 |
. . . . . . . . . . 11
β’ (π β πΈ β ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ) = β¨(1st
βπ), (πβ(2nd
βπ))β©) |
28 | 12, 27 | syl 17 |
. . . . . . . . . 10
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ) = β¨(1st
βπ), (πβ(2nd
βπ))β©) |
29 | 28 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ)) = (πββ¨(1st βπ), (πβ(2nd βπ))β©)) |
30 | | xp1st 8007 |
. . . . . . . . . . . . 13
β’ (π β ((mTCβπ) Γ (mRExβπ)) β (1st
βπ) β
(mTCβπ)) |
31 | 16, 30 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (1st βπ) β (mTCβπ)) |
32 | 2, 14 | mrsubf 34539 |
. . . . . . . . . . . . . 14
β’ (π β ran (mRSubstβπ) β π:(mRExβπ)βΆ(mRExβπ)) |
33 | 11, 32 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β π:(mRExβπ)βΆ(mRExβπ)) |
34 | 17, 15 | eleq2s 2852 |
. . . . . . . . . . . . . 14
β’ (π β πΈ β (2nd βπ) β (mRExβπ)) |
35 | 12, 34 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (2nd βπ) β (mRExβπ)) |
36 | 33, 35 | ffvelcdmd 7088 |
. . . . . . . . . . . 12
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (πβ(2nd βπ)) β (mRExβπ)) |
37 | | opelxpi 5714 |
. . . . . . . . . . . 12
β’
(((1st βπ) β (mTCβπ) β§ (πβ(2nd βπ)) β (mRExβπ)) β β¨(1st
βπ), (πβ(2nd
βπ))β© β
((mTCβπ) Γ
(mRExβπ))) |
38 | 31, 36, 37 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β β¨(1st βπ), (πβ(2nd βπ))β© β
((mTCβπ) Γ
(mRExβπ))) |
39 | 38, 15 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β β¨(1st βπ), (πβ(2nd βπ))β© β πΈ) |
40 | | msubvrs.v |
. . . . . . . . . . 11
β’ π = (mVarsβπ) |
41 | 19, 1, 40 | mvrsval 34527 |
. . . . . . . . . 10
β’
(β¨(1st βπ), (πβ(2nd βπ))β© β πΈ β (πββ¨(1st βπ), (πβ(2nd βπ))β©) = (ran (2nd
ββ¨(1st βπ), (πβ(2nd βπ))β©) β© (mVRβπ))) |
42 | 39, 41 | syl 17 |
. . . . . . . . 9
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (πββ¨(1st βπ), (πβ(2nd βπ))β©) = (ran (2nd
ββ¨(1st βπ), (πβ(2nd βπ))β©) β© (mVRβπ))) |
43 | | fvex 6905 |
. . . . . . . . . . . . 13
β’
(1st βπ) β V |
44 | | fvex 6905 |
. . . . . . . . . . . . 13
β’ (πβ(2nd
βπ)) β
V |
45 | 43, 44 | op2nd 7984 |
. . . . . . . . . . . 12
β’
(2nd ββ¨(1st βπ), (πβ(2nd βπ))β©) = (πβ(2nd βπ)) |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (2nd
ββ¨(1st βπ), (πβ(2nd βπ))β©) = (πβ(2nd βπ))) |
47 | 46 | rneqd 5938 |
. . . . . . . . . 10
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β ran (2nd
ββ¨(1st βπ), (πβ(2nd βπ))β©) = ran (πβ(2nd
βπ))) |
48 | 47 | ineq1d 4212 |
. . . . . . . . 9
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (ran (2nd
ββ¨(1st βπ), (πβ(2nd βπ))β©) β© (mVRβπ)) = (ran (πβ(2nd βπ)) β© (mVRβπ))) |
49 | 29, 42, 48 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ)) = (ran (πβ(2nd βπ)) β© (mVRβπ))) |
50 | 19, 1, 40 | mvrsval 34527 |
. . . . . . . . . . 11
β’ (π β πΈ β (πβπ) = (ran (2nd βπ) β© (mVRβπ))) |
51 | 12, 50 | syl 17 |
. . . . . . . . . 10
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (πβπ) = (ran (2nd βπ) β© (mVRβπ))) |
52 | 51 | iuneq1d 5025 |
. . . . . . . . 9
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β βͺ
π₯ β (πβπ)(πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯))) = βͺ
π₯ β (ran
(2nd βπ)
β© (mVRβπ))(πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯)))) |
53 | | msubvrs.h |
. . . . . . . . . . . . . . . . 17
β’ π» = (mVHβπ) |
54 | 19, 1, 53 | mvhf 34580 |
. . . . . . . . . . . . . . . 16
β’ (π β mFS β π»:(mVRβπ)βΆπΈ) |
55 | 54 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β π»:(mVRβπ)βΆπΈ) |
56 | | inss2 4230 |
. . . . . . . . . . . . . . . 16
β’ (ran
(2nd βπ)
β© (mVRβπ))
β (mVRβπ) |
57 | 56 | sseli 3979 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (ran (2nd
βπ) β©
(mVRβπ)) β π₯ β (mVRβπ)) |
58 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . 15
β’ ((π»:(mVRβπ)βΆπΈ β§ π₯ β (mVRβπ)) β (π»βπ₯) β πΈ) |
59 | 55, 57, 58 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (π»βπ₯) β πΈ) |
60 | | fveq2 6892 |
. . . . . . . . . . . . . . . 16
β’ (π = (π»βπ₯) β (1st βπ) = (1st
β(π»βπ₯))) |
61 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . 16
β’ (π = (π»βπ₯) β (πβ(2nd βπ)) = (πβ(2nd β(π»βπ₯)))) |
62 | 60, 61 | opeq12d 4882 |
. . . . . . . . . . . . . . 15
β’ (π = (π»βπ₯) β β¨(1st βπ), (πβ(2nd βπ))β© = β¨(1st
β(π»βπ₯)), (πβ(2nd β(π»βπ₯)))β©) |
63 | 62, 25, 26 | fvmpt3i 7004 |
. . . . . . . . . . . . . 14
β’ ((π»βπ₯) β πΈ β ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯)) = β¨(1st β(π»βπ₯)), (πβ(2nd β(π»βπ₯)))β©) |
64 | 59, 63 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯)) = β¨(1st β(π»βπ₯)), (πβ(2nd β(π»βπ₯)))β©) |
65 | 57 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β π₯ β (mVRβπ)) |
66 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(mTypeβπ) =
(mTypeβπ) |
67 | 19, 66, 53 | mvhval 34556 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (mVRβπ) β (π»βπ₯) = β¨((mTypeβπ)βπ₯), β¨βπ₯ββ©β©) |
68 | 65, 67 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (π»βπ₯) = β¨((mTypeβπ)βπ₯), β¨βπ₯ββ©β©) |
69 | | fvex 6905 |
. . . . . . . . . . . . . . . 16
β’
((mTypeβπ)βπ₯) β V |
70 | | s1cli 14555 |
. . . . . . . . . . . . . . . . 17
β’
β¨βπ₯ββ© β Word V |
71 | 70 | elexi 3494 |
. . . . . . . . . . . . . . . 16
β’
β¨βπ₯ββ© β V |
72 | 69, 71 | op1std 7985 |
. . . . . . . . . . . . . . 15
β’ ((π»βπ₯) = β¨((mTypeβπ)βπ₯), β¨βπ₯ββ©β© β (1st
β(π»βπ₯)) = ((mTypeβπ)βπ₯)) |
73 | 68, 72 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (1st
β(π»βπ₯)) = ((mTypeβπ)βπ₯)) |
74 | 69, 71 | op2ndd 7986 |
. . . . . . . . . . . . . . . 16
β’ ((π»βπ₯) = β¨((mTypeβπ)βπ₯), β¨βπ₯ββ©β© β (2nd
β(π»βπ₯)) = β¨βπ₯ββ©) |
75 | 68, 74 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (2nd
β(π»βπ₯)) = β¨βπ₯ββ©) |
76 | 75 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (πβ(2nd β(π»βπ₯))) = (πββ¨βπ₯ββ©)) |
77 | 73, 76 | opeq12d 4882 |
. . . . . . . . . . . . 13
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β β¨(1st
β(π»βπ₯)), (πβ(2nd β(π»βπ₯)))β© = β¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) |
78 | 64, 77 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯)) = β¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) |
79 | 78 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯))) = (πββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©)) |
80 | | simpl1 1192 |
. . . . . . . . . . . . . . . 16
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β π β mFS) |
81 | 19, 13, 66 | mtyf2 34573 |
. . . . . . . . . . . . . . . 16
β’ (π β mFS β
(mTypeβπ):(mVRβπ)βΆ(mTCβπ)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (mTypeβπ):(mVRβπ)βΆ(mTCβπ)) |
83 | 82, 65 | ffvelcdmd 7088 |
. . . . . . . . . . . . . 14
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β ((mTypeβπ)βπ₯) β (mTCβπ)) |
84 | 33 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β π:(mRExβπ)βΆ(mRExβπ)) |
85 | | elun2 4178 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (mVRβπ) β π₯ β ((mCNβπ) βͺ (mVRβπ))) |
86 | 65, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β π₯ β ((mCNβπ) βͺ (mVRβπ))) |
87 | 86 | s1cld 14553 |
. . . . . . . . . . . . . . . 16
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β β¨βπ₯ββ© β Word
((mCNβπ) βͺ
(mVRβπ))) |
88 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(mCNβπ) =
(mCNβπ) |
89 | 88, 19, 14 | mrexval 34523 |
. . . . . . . . . . . . . . . . 17
β’ (π β mFS β
(mRExβπ) = Word
((mCNβπ) βͺ
(mVRβπ))) |
90 | 80, 89 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (mRExβπ) = Word ((mCNβπ) βͺ (mVRβπ))) |
91 | 87, 90 | eleqtrrd 2837 |
. . . . . . . . . . . . . . 15
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β β¨βπ₯ββ© β
(mRExβπ)) |
92 | 84, 91 | ffvelcdmd 7088 |
. . . . . . . . . . . . . 14
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (πββ¨βπ₯ββ©) β (mRExβπ)) |
93 | | opelxpi 5714 |
. . . . . . . . . . . . . 14
β’
((((mTypeβπ)βπ₯) β (mTCβπ) β§ (πββ¨βπ₯ββ©) β (mRExβπ)) β
β¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β© β ((mTCβπ) Γ (mRExβπ))) |
94 | 83, 92, 93 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β
β¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β© β ((mTCβπ) Γ (mRExβπ))) |
95 | 94, 15 | eleqtrrdi 2845 |
. . . . . . . . . . . 12
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β
β¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β© β πΈ) |
96 | 19, 1, 40 | mvrsval 34527 |
. . . . . . . . . . . 12
β’
(β¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β© β πΈ β (πββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) = (ran (2nd
ββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) β© (mVRβπ))) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . 11
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (πββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) = (ran (2nd
ββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) β© (mVRβπ))) |
98 | | fvex 6905 |
. . . . . . . . . . . . . . 15
β’ (πββ¨βπ₯ββ©) β
V |
99 | 69, 98 | op2nd 7984 |
. . . . . . . . . . . . . 14
β’
(2nd ββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) = (πββ¨βπ₯ββ©) |
100 | 99 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (2nd
ββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) = (πββ¨βπ₯ββ©)) |
101 | 100 | rneqd 5938 |
. . . . . . . . . . . 12
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β ran (2nd
ββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) = ran (πββ¨βπ₯ββ©)) |
102 | 101 | ineq1d 4212 |
. . . . . . . . . . 11
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (ran (2nd
ββ¨((mTypeβπ)βπ₯), (πββ¨βπ₯ββ©)β©) β© (mVRβπ)) = (ran (πββ¨βπ₯ββ©) β© (mVRβπ))) |
103 | 79, 97, 102 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β§ π₯ β (ran (2nd βπ) β© (mVRβπ))) β (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯))) = (ran (πββ¨βπ₯ββ©) β© (mVRβπ))) |
104 | 103 | iuneq2dv 5022 |
. . . . . . . . 9
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β βͺ
π₯ β (ran
(2nd βπ)
β© (mVRβπ))(πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯))) = βͺ
π₯ β (ran
(2nd βπ)
β© (mVRβπ))(ran
(πββ¨βπ₯ββ©) β©
(mVRβπ))) |
105 | 52, 104 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β βͺ
π₯ β (πβπ)(πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯))) = βͺ
π₯ β (ran
(2nd βπ)
β© (mVRβπ))(ran
(πββ¨βπ₯ββ©) β©
(mVRβπ))) |
106 | 21, 49, 105 | 3eqtr4d 2783 |
. . . . . . 7
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ)) = βͺ π₯ β (πβπ)(πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯)))) |
107 | | fveq1 6891 |
. . . . . . . . 9
β’ (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (πΉβπ) = ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ)) |
108 | 107 | fveq2d 6896 |
. . . . . . . 8
β’ (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (πβ(πΉβπ)) = (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ))) |
109 | | fveq1 6891 |
. . . . . . . . . 10
β’ (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (πΉβ(π»βπ₯)) = ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯))) |
110 | 109 | fveq2d 6896 |
. . . . . . . . 9
β’ (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (πβ(πΉβ(π»βπ₯))) = (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯)))) |
111 | 110 | iuneq2d 5027 |
. . . . . . . 8
β’ (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β βͺ π₯ β (πβπ)(πβ(πΉβ(π»βπ₯))) = βͺ
π₯ β (πβπ)(πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯)))) |
112 | 108, 111 | eqeq12d 2749 |
. . . . . . 7
β’ (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β ((πβ(πΉβπ)) = βͺ
π₯ β (πβπ)(πβ(πΉβ(π»βπ₯))) β (πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)βπ)) = βͺ π₯ β (πβπ)(πβ((π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©)β(π»βπ₯))))) |
113 | 106, 112 | syl5ibrcom 246 |
. . . . . 6
β’ ((π β mFS β§ π β ran (mRSubstβπ) β§ π β πΈ) β (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (πβ(πΉβπ)) = βͺ
π₯ β (πβπ)(πβ(πΉβ(π»βπ₯))))) |
114 | 113 | 3expia 1122 |
. . . . 5
β’ ((π β mFS β§ π β ran (mRSubstβπ)) β (π β πΈ β (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (πβ(πΉβπ)) = βͺ
π₯ β (πβπ)(πβ(πΉβ(π»βπ₯)))))) |
115 | 114 | com23 86 |
. . . 4
β’ ((π β mFS β§ π β ran (mRSubstβπ)) β (πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (π β πΈ β (πβ(πΉβπ)) = βͺ
π₯ β (πβπ)(πβ(πΉβ(π»βπ₯)))))) |
116 | 115 | rexlimdva 3156 |
. . 3
β’ (π β mFS β (βπ β ran (mRSubstβπ)πΉ = (π β πΈ β¦ β¨(1st βπ), (πβ(2nd βπ))β©) β (π β πΈ β (πβ(πΉβπ)) = βͺ
π₯ β (πβπ)(πβ(πΉβ(π»βπ₯)))))) |
117 | 10, 116 | biimtrid 241 |
. 2
β’ (π β mFS β (πΉ β ran π β (π β πΈ β (πβ(πΉβπ)) = βͺ
π₯ β (πβπ)(πβ(πΉβ(π»βπ₯)))))) |
118 | 117 | 3imp 1112 |
1
β’ ((π β mFS β§ πΉ β ran π β§ π β πΈ) β (πβ(πΉβπ)) = βͺ
π₯ β (πβπ)(πβ(πΉβ(π»βπ₯)))) |